A Hoare-style verification calculus for control state ASMs
Werner Gabrisch, Wolf Zimmermann · 2012
We present a Hoare-style calculus for control-state Abstract State Machines (ASM) such that verification of control-state ASMs is possible. In particular, a Hoare-Triple {φ}A{ψ} for an ASM A means that if an initial state T satisfies the precondition φ and a final state F is reached by A, then the final state satisfies the postcondition ψ. While it is straightforward to generalize the assignment axiom of the Hoare-Calculus to a single state transition, the composition of Hoare-Triples is challenging since typical programming language concepts are not present in ASMs.