Formal Development and Verification of Reusable Component in PAR Platform

Formal method is an important approach to develop high trust software systems. Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. Set, Bag, List, Tree, Graph are important reusable components in PAR platform. This paper tries to formally develop ‘Set’ components which have linear structure and verify the correctness of this component mechanically with Coq. The formal development of this component involves formalization of specification, the recurrence relation of problem-solving sequence and loop invariant. Specification language Radl of PAR platform was used to describe the specification, recurrence relation and loop invariants; Software modelling language Apla was used to describe the abstract model of those components. The Dijkstra’s Weakest Precondition method is used to verify abstract model by the interactive proof tool Coq. Finally, the abstract model denoted by Apla was transformed to concrete model written by executable language; such as C++, Java, VB and C#, etc., based on the program generating systems in PAR platform.