Allowing State Changes in Specifications

Abstract. We provide a static analysis (using both dataflow analysis and theorem proving) to allow state changes within specifications. This can be used for specification languages that share the same expression sub-language with an implementation language so that method calls can appear in preconditions, postconditions, and object invariants without violating the soundness of the system.

• Type: Conference
• Year: 2006
• Where: ETRICS
• Authors: Michael Barnett, David A. Naumann, Wolfram Schulte, Qi Sun
• Keywords: Dataflow Analysis, ETRICS 2006, Security Privacy, Static Analysis, Theorem Proving