+1 Recommend
1 collections
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Verifying Invariant Based Programs in the SOCOS Environment

      , ,

      Teaching Formal Methods: Practice and Experience (TFM)

      Teaching Formal Methods: Practice and Experience

      15 December 2006

      Invariant based programming, verification, SOCOS

      Read this article at

          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.


          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.

          Related collections

          Most cited references 4

          • Record: found
          • Abstract: not found
          • Article: not found

          Simplify: a theorem prover for program checking

            • Record: found
            • Abstract: not found
            • Conference Proceedings: not found

            Extended static checking for Java

              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Incremental Software Construction with Refinement Diagrams


                Author and article information

                December 2006
                December 2006
                : 1-6
                Turku Centre for Computer Science

                Åbo Akademi University, Department of Information Technologies

                Joukahaisenkatu 3-5 A, FIN-20520, Turku, Finland
                © Ralph-Johan Back et al. Published by BCS Learning and Development Ltd. Teaching Formal Methods: Practice and Experience, BCS London Office, UK

                This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

                Teaching Formal Methods: Practice and Experience
                BCS London Office, UK
                15 December 2006
                Electronic Workshops in Computing (eWiC)
                Teaching Formal Methods: Practice and Experience
                Product Information: 1477-9358BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Electronic Workshops in Computing


                Comment on this article