(WIP) Encode spec items as methods

[Aurel300]

I separated this out from #127 because it's not really related and causes some tests to fail. Some TODOs:

• when encoding the method for a spec item, the previous spec items in the contract should be added as well; for example, preconditions might justify the well-formedness of a postcondition (e.g., this postcondition depends on this precondition)
• properly deal with encoding spec-only constructs (like quantifiers)