[SAL] Some questions for using SAL

[harry huang]

Hi,

I have some questions regarding the SAL.

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.

2. Is there way to express the wait condition ? For instance, I want to 
express the java expression "while ( a != 0) wait();" in SAL . Anway, I saw 
example that has "sleeping, trying, critical ". Are those keywords SAL 
reserved keywords or user defined ?

3. How to expression the invariant in SAL ? Does the invariant can be 
defined in DEFINITION ?

4. Is there "for" loop in SAL ?

Thanks.

Harry