Statement inversion and strongest postcondition (Q1261493)

The paper presents the notion of inverse commands for a language permitting both demonic and angelic nondeterminism as well as miracles and nontermination within the general framework of Dijkstra's weakest precondition calculus. By incorporating different types of nondeterminism into the calculus, it may be applied even to non-executable program constructs. Additionally, by the same token, arbitrary input-output specifications, data refinement and parallel programs can be treated within the extended calculus. An inverse command \(S^{-1}\) of a command \(S\) is defined as \(S^{-1}\); \(S\leq skip\leq S\); \(S^{-1}\) where \(\leq\) is the refinement relation. In brief, a program \(S-1\) is the (true) inverse of a program \(S\) if it computes the input \(S\), given the output. \(S\) is not invertible, it its input is not defined uniquely by its output. Angelic nondeterminism and miraculously terminating commands allow for the inversion of a program even though its input is not uniquely determined by its output. Firmly rooted in the total correctness framework of the refinement calculus, generalised inverses which exist for all conjunctive commands are defined for arbitrary commands of this kind. Eventually, rules are given for computing inverses that can be used to describe data refinement between commands.