Deriving Partial Correctness Logics From Evolving Algebras.
Arnd Poetzsch‐Heffter · 1994
Introduction This extended abstract gives an introduction into the development of partial correctness logics for programming languages specified by evolving algebras. A partial correctness logic is a programming logic that allows to prove program properties of the form: "whenever program point P is reached during execution, assertion A is true". We derive a basic axiom (schema) from an evolving algebra and use this axiom to prove more convenient logics correct. This work aims to develop the foundations for programming environments that support formal reasoning about programs. One of the major problems with this challenge is the systematic design of programming logics for realistic programming languages. Experiences e.g. with Hoare logic have shown that it can be difficult to design consistent programming logics even for simple languages from scratch (cf. [1]). Using evolving algebras as semantical basis has two advantages: 1. They support appropriate specificat