[SAL] Some questions for using SAL
harryh23 at hotmail.com
Sat Jun 17 06:53:35 PDT 2006
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 ?
More information about the SAL