A Prospective-Value Semantics for the GSL
We present a prospective-value (pv) semantics for the Generalised Substitution Language. Whereas wp semantics captures the meaning of a computation in terms of the weakest precondition that must be fulfilled for a generalised substitution S to establish any given postcondition Q, pv semantics expresses the meaning of a computation in terms of the value any expression E would take were the computation to be carried out. To integrate non-termination we formulate improper bunch theory, an extended version of Hehner’s bunch theory where each type is augmented with an improper bunch. Algebraic simplification laws for the pv expression transformer are presented, and proved to be sound. Iteration is treated as a fixed-point in expressions, and a corresponding theorem is presented allowing us to infer the pv effect of the while-loop construct.
KeywordsGeneralised substitution bunch theory prospective-value semantics expression transformers wp calculus B Method
Unable to display preview. Download preview PDF.