Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Allowing State Changes in Specifications

Michael Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun

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.

Details

Publication typeInproceedings
Published inETRICS
Pages321-336
Volume3995
SeriesLecture Notes in Computer Science
ISBN3-540-34640-6
PublisherSpringer
> Publications > Allowing State Changes in Specifications