Allowing State Changes in Specifications

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.

AllowingStateChanges(ETRICS2006).pdf
PDF file

In  ETRICS

Publisher  Springer

Details

TypeInproceedings
Pages321-336
Volume3995
SeriesLecture Notes in Computer Science
ISBN3-540-34640-6
> Publications > Allowing State Changes in Specifications