Michael Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun
2006
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.
![]() PDF file |
In: ETRICS
Publisher: Springer
| Type: | Inproceedings |
| Pages: | 321-336 |
| Volume: | 3995 |
| Series: | Lecture Notes in Computer Science |
| ISBN: | 3-540-34640-6 |