OBSCURE, a specification language for abstract data types (Q1323328)

OBSCURE is a specification language for abstract data types. It differs from classical specification languages by handling models rather than theories. The goal of the paper is to present a complete and precise description of OBSCURE. First, the different language constructs are illustrated by the help of examples. The syntax and semantics of the language are then defined formally. The consistency of these definitions is stated in two theorems. Next, a set of formulas is associated with each specification. A further theorem states that these formulas guarantee the persistency or, more precisely, the absence of logical inconsistencies. A discussion of further language concepts -- such as parameterization and strong typing - - follows. Finally, a methodology for the development of software with the help of OBSCURE is sketched and some practical results are presented.