Ina Jo Specification Language: A Critical Study

摘要

Ina Jo, a language for formal specification and verification, provides a lucid vehicle for the logical description of software systems under design. This paper gives a self-contained critical account of the full range of features of the language Concrete examples illustrate its strengths and weaknesses, and an approach to giving a formal semantics for the language is sketched. The paper addresses issues fundamental to the design of specification languages, but is also suitable as a tutorial introduction to the Ina Jo language.