Facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specification is a difficult task. This paper presents the formal software specification language LFC which is designed to support the acquisition and validation of formal specifications. LFC relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect and uses context-free languages for syntactic aspect of specifications. Specification in LFC and the validation are entirely machine-aided. Specification is mainly facilitated through grammatical learning technique and case-driven technique for function construction. Validation is facilitated by sample recognition and generation techniques and rapid prototyping technique. A formal specification acquisition system SAQ has been implemented, several non-trivial examples have been developed using SAQ.

• Type: Journal
• Year: 2006
• Where: KBS
• Authors: Haiming Chen, Yunmei Dong
• Keywords: Formal Specification, Formal Specification Techniques, KBS 2006, Recursive Functions