Testing and verifying invariant based programs in the SOCOS environment

An invariant based program is a state transition diagram consisting of nested situations (predicates over program variables) and transitions between situations (predicate transformers). Reasoning about correctness is performed in a local fashion by examining each situation at a time and proving that the situation is satisfied for all possible executions. Since the invariants are in place from the beginning and the verification conditions are easily extracted from the diagram there is no need for complicated proof rules, making invariant diagrams a suitable notation for introducing formal verification to students and programmers. Our preliminary experience from using invariant diagrams in the classroom has prompted the need for a tool to support the method: we introduce here SOCOS, an environment for invariant based programming. SOCOS generates correctness conditions based on weakest precondition semantics, and the user can attempt to automatically discharge these conditions using the Simplify theorem prover; conditions which were not automatically discharged can be proved interactively in the PVS theorem prover