Title :
PK/C++: an object-oriented, logic-based, executable specification language
Author :
Terwilliger, Robert B. ; Kirslis, Peter A.
Author_Institution :
Dept. of Comput. Sci., Colorado Univ., Boulder, CO, USA
Abstract :
ENCOMPASS is an environment that supports software development using formal techniques similar to the Vienna development method (VDM). In ENCOMPASS, software can be specified using the PLEASE family of executable specification languages, PK/C++, the latest number of the PLEASE family, differs from its predecessor by having C++ rather than Ada as its base language, by having an operational as well as declarative semantics, and by being based on flat rather than standard Prolog. PK/C++ specifications can be used in proofs of correctness. They are also executable, so that initial specifications can be validated and refinements can be verified using testing-based techniques. The authors give an overview of ENCOMPASS, describe PK/C++ in reasonable detail, and give an example of development using the language
Keywords :
C language; C listings; formal specification; object-oriented programming; programming environments; software packages; specification languages; ENCOMPASS; PK/C++ specifications; PLEASE family; VDM; Vienna development method; base language; correctness; declarative semantics; executable specification languages; formal techniques; logic-based; object-oriented; software development; testing-based techniques; Computer science; Logic programming; Production; Prototypes; Software prototyping; Software quality; Specification languages; Testing; Trademarks; US Government;
Conference_Titel :
System Sciences, 1989. Vol.II: Software Track, Proceedings of the Twenty-Second Annual Hawaii International Conference on
Conference_Location :
Kailua-Kona, HI
Print_ISBN :
0-8186-1912-0
DOI :
10.1109/HICSS.1989.48019
