PK/C++: an Object-Oriented, Logic-Based, Executable Specification Language
01 January 1989
The ENCOMPASS project has been developing languages and environments to support formal development methods similar to VDM since the mid 1980s. PK/C++ is the latest member of the PLEASE family; these excutable specification languages support software development by incremental refinement. PK/C++ differs from its predecessor by being based on C++ rather than Ada(R), having an operational as well as declarative semantics, and being based on flat rather than standard Prolog. Using PK/C++, software components are first specified using a combination of conventional programming languages and predicate logic.