Last time I started discussing the expression language used to define predicates on types and members. My conclusions were:
C# expression syntax used since code must be transformed to that in the end, and the more similar the syntaxes of the expression language - the easier the transformation will be.
No side-effects. Side effect within the predicates complicate the tasks of determining whether a temporal comparison is actually effective. If the snapshots can’t be guaranteed to be faithful representations of the state before and after the test, then you can’t trust the tests, and you might as well not have bothered with them in the first place.
Pragmas, or pre-processor messages, are used in expressions to add a temporal ability to the predicates. $before(foo) allows a snapshot of the variable foo to be taken for later comparison with the exit state.
Pragmas may map to identity in some circumstances. Entry states can have no $after() since we haven’t reached the exit state yet. Likewise, there is no notion $before() state since this is the before state, and we can’t take a snapshot of the state before the before state (unless it’s on some other superior method). Therefore, in a precondition it should be illegal to insert pragmas into predicate expressions. In some cases such as $before(foo) in a precondition, and $after(bar) in a post condition the pragmas map onto the current value of the variable. i.e. in a post condition $after(bar) can be transformed into bar.
The algorithm for converting predicates to guard code is shown below.
foreach assembly in assembly list foreach type in assembly clear list of invariance predicates clear list of processed methods foreach invariant attribute on type transform pragmas on predicate add pre/post analysis objs to list generate code for predicate append code to processedInvariants list end foreach invariant foreach member in type clear list of requires attrs foreach requires attr on member transform pragmas on predicate add pre/post analysis objs to list generate code for predicate append code to processedRequires list end foreach requires attr clear list of ensures attrs foreach ensures attr on member transform pragmas on predicate extract list of vars to be snapshot add to list processedSnapshots add pre/post analysis objs to list generate code for predicate append code to processedEnsures list end foreach ensures attr insert snapshots into code template insert pre/post analysis objs to template insert code for requires guards into template insert code for ensures guards into template generate code add generated code to processed methods list end foreach member insert code for members into type template clear list of invariance predicates generate code for type append code to processed types list end foreach type setup c# compiler with config params compile all types in processed types list store assembly as per instructions end foreach assembly
This algorithm conveniently glosses over the complexities of the depth first search event propagation mechanism described in previous posts, but the outcome is the same ultimately.