[SAL] Re: Some questions for using SAL

[harry huang]

Hi David,

Thanks. I still have two questions regarding (3), (4). For (3), is it 
possible to define the invariant in "DEFINITION" ? I saw the SAL language 
manual said something about it . For (4), can you give me explicitly SAL 
semantics for "for (int i =0; i <10; i++) System.out.println("hello")" in 
Java ?

In addition, in the tutorial it mentions that SAL is a framework for model 
checking and theorem proving. But how can I apply theorem proving techniques 
in SAL ?

Thanks.

Harry



>From: David Friggens <David.Friggens at mcs.vuw.ac.nz>
>To: sal at csl.sri.com
>CC: harry huang <harryh23 at hotmail.com>
>Subject: [SAL] Re: Some questions for using SAL
>Date: Sun, 18 Jun 2006 11:22:28 +1200
>
>Hi Harry
>
> > I have some questions regarding the SAL.
>
>Hopefully I can answer some of your questions. First, I'll point out
>that SAL is not a procedural language - you define the transitions by
>writing the changes that happen to the variables. If you want to model
>some code from a procedural language you'll need to define a program
>counter variable. Then you can define transitions from location1 to
>location2, from location2 to location3, etc.
>
>The msclock example (in SAL 2.4) is a good example of this.
>
> > 1. Can I write the assertion in the module ? For instance, I want to
> > express "assert(a==b)", how to write it in module as I see the
> > example that the assertion written in the Theorem.
>
>You can put a=b in the guard of the transition, and have another one
>that goes to an error state. For example
>
>pc = locX AND a = b --> pc' = locY
>
>and
>
>pc = locX AND a /= b --> pc' = locError
>
>Then you could test that the module doesn't ever enter the error state:
>THEOREM system |- G(pc /= locError)
>
>
> > 2. Is there way to express the wait condition ? For instance, I want
> > to express the java expression "while ( a != 0) wait();" in SAL .
>
>You could use a transition like:
>
>pc = locX AND a = 0 --> pc' = locY
>
>This transition is only enabled if the module is at location locX and a
>is zero, so if it's at locX and a isn't zero, then it has to wait until
>a transition becomes enabled (i.e. when a becomes zero).
>
> > Anway, I saw example that has "sleeping, trying, critical ". Are
> > those keywords SAL reserved keywords or user defined ?
>
>These are user defined.
>
> > 3. How to expression the invariant in SAL ?
>
>If you want to prove that a property "p" is an invariant you can use the
>LTL formula G(p). For example
>THEOREM system |- G(a <= 5 AND b >= 10).
>
> > 4. Is there "for" loop in SAL ?
>
>Not explicitly, but you can express it easily.
>
>
>Cheers
>David
>