Design and Implementation of the Foraml Specification Acquisition System SAQ

摘要

The formal specification acquisition system SAQ is designed to assist users to acquire and verify specifications with support of specification bases. In SAQ, specifications are represented by context-free languages and recursive functions defined on context-free languages, which are called concepts and operations defined on concepts respectively. Acquisition of specifications is ocmpleted by human-machine cooperation, based on specification reuse. Concepts are verified by sample recognition and generation, and operations are verified by applying operations on samples of concepts. The design and key implementation techniques of SAQ are introduced, experiments are presented.