Title :
Correctness of full first-order specifications
Author_Institution :
Inst. fur Logik, Karlsruhe Univ., Germany
Abstract :
Investigates an algebraic specification method for abstract data types which is designed for the application in formal software development. The specification language is full first-order logic, and the semantics of a specification is the class of its generated models. Full first-order specifications are more flexible than Horn clause specifications and exhibit better deductive properties. The author presents criteria for the correctness of full first-order specifications and for the incremental development of large specifications from smaller ones
Keywords :
abstract data types; formal logic; formal specification; specification languages; Horn clause specifications; abstract data types; algebraic specification; formal software development; full first-order logic; full first-order specifications; semantics; specification language; Algebra; Application software; Design methodology; Equations; Logic; Logic design; Logic functions; Programming; Sections; Specification languages;
Conference_Titel :
Software Engineering and Knowledge Engineering, 1992. Proceedings., Fourth International Conference on
Conference_Location :
Capri
Print_ISBN :
0-8186-2830-8
DOI :
10.1109/SEKE.1992.227918
