Package generator provides the functions necessary for generating contracts.

Package parser implements contract parsing.

NewEnsures creates a Ensures object.

NewFuncContract creates a FuncContract.

NewLet creates a Let object Contract: - requires expr != "".

NewRequires creates a Requires object.

NewTypeContract creates a TypeContract.

OldCounter the counter to use when creating old_ parameters TODO: use a more elegant approach.

Re4old is a regular expression for @old expressions.

Ensures is a @ensures clause of a contract.

FuncContract represents a contract associated to a function.

Let models a @Let clause.

Requires is a @requires clause of a contract.

TypeContract represents a contract associated to a type.