Function contracts

reads( ... )


writes( ... )


requires( ... )


ensures( ... )


maintains( ... )


returns( ... )

Annotations to functions

ispure


frameaxiom


See Pure functions

Last edited Sep 3, 2009 at 1:17 PM by MichalMoskal, version 2

Comments

No comments yet.