Eiffel - as well as other object-oriented languages - have a built-in support for higher-order implementations through function objects. These are called agents in Eiffel. As with other functions, these can have pre- and postconditions.
Although the problem of static verification of function objects has been solved for functional programming languages, these solutions cannot be applied to object-oriented languages due the use of the heap and side effects. Agents are therefore diffcult to prove.
In Reasoning about Function Objects, a novel approach is described which uses side effect free (pure) routines to specify the pre- and postconditions of agents. To specify routines that take agents as arguments, these pure routines are used.
The master thesis focuses on the techniques described in Reasoning about Function Objects. This verification methodology for agents will be implemented in Ballet to allow static verification of agents. Also, the methodology will be extended to allow a generic argument count and return values. Instead of having Ballet as a standalone modification of EiffelStudio, it will be integrated in the ETH Verification Environment (EVE).
As optional parts of the thesis, the specification language will be extended with modifies clauses, and non- interference will be implemented.
As Ballet is based on Boogie which currently only runs on Windows, the verification will for the moment only run on Windows.