This is an old revision of the document!
Modular analysis of procedures
Inlining specifications. Last part of SAV07 Homework 4.
Postconditions that refer to values of variables in the precondition.
The meaning of modifies clauses.
ASTREE Static Analyzer
The Octagon Abstract Domain
A Static Analyzer for Large Safety-Critical Software
Section 5.4: A remark on notation:
- if denotes the state and is a deterministic statement, then represents the new state after executing the statement; the relation corresponding to statement semantics would be .
- this function is extended to map sets of states to sets of states, which gives function mapping to and is what we called strongest postcondition .
- this is abstracted to abstract domain