Abstract
Hehner's theory of predicative programming is a general-purpose refinement calculus for producing correct sequential, concurrent, real-time, and communicating programs from specifications. However, only limited tool support exists for this theory. We give an overview of an ongoing project on how we are providing support for predicative programming via PVS, particularly for discharging the proof obligations that arise during algorithm refinement, and specifically, in the domain of real-time...
Users
Please
log in to take part in the discussion (add own reviews or comments).