Static class invariants and class local invariants in the Spec#

Sep 19, 2012 at 8:49 AM

Hello,

I am reading "Modular Verification of Static Class Invariants" and "Class-Local Object Invariants" papers and would like to try the examples from the papers.

Are these implemented in Spec# tool? If yes, is it possible to find syntax examples somewhere?

Thank you,

Boriss 

 

Developer
Sep 19, 2012 at 1:50 PM

Hi Boriss,

Unfortunately we never got around to implementing the static class invariants. However, the class-local object invariants are implemented. In fact, the expose statement in Spec# is a local expose that uses the static type of the expression to determine the class frame that gets exposed (the other one is called additive expose), and fields are by default non-additive (use the [Additive] attribute to make a field additive). A short discussion is contained in the Spec# tutorial (http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=LeinoMueller09a.pdf, page 23).

You can find examples for additive fields/expose/invariants in the SscBoogie\Test directory, e.g., tutorial\Sec2.2-Additive.ssc. Most other examples in the tutorial folder show the use of non-additive fields/expose/invariants.

Cheers,
    Peter