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. © Springer-Verlag Berlin Heidelberg 2006.
Cite
CITATION STYLE
Barnett, M., Naumann, D. A., Schulte, W., & Sun, Q. (2006). Allowing state changes in specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3995 LNCS, pp. 321–336). Springer Verlag. https://doi.org/10.1007/11766155_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
