Group P.1 - Assertion control capabilities issues
Issues
49, 66, 67, 122.
Discussion
Minutes of meetings on Group P.1:
An initial list of requirements was proposed.
See (here) for more details.
Triggering procedural blocks
The initial suggestion
Triggering a procedural block on the empty word:
- In the meeting on 25.7.06 it was suggested to adopt the SVA semantics and not trigger procedural blocks on the empty word. see details
(here)
- Cindy: in {a;b[*]$A$;c}, 'A' should be triggered after each 'a' (because we have seen b[*]).
- Johan: If we adopt the SVA expansion rule for psl we would have b[*]$A$ ==> b[*]:1$A$. one could still express
what Cindy is suggesting by
(a;b[*])$A$;c
- Dmitry P: A problem in SVA's semantics: while a;b[*];c holds on the trace 'ac', a;b[*]$A$;c does not hold on this trace, because it requires a cycle
between the occurences of a and c. That is, adding a procedural block to the sequence changes its semantics.
- Dana: To avoid this problem the syntax should require the procedural block to be attached to a certain boolean expression rather than a certain sub-sere.
- Dmitry P: the requirement on R to be a simple boolean is too restrictive. It is not possible to write things like b[*2]$A$.
- We thought of separating p.b. into two cathegories: "pure" and
"impure" procedural blocks.
- Pure procedural blocks are guaranteed not to change the model (change of
local variable is not considered model change). Tools should ensure this
policy is not violated.
- Impure procedural blocks are totally free and can do everything.
- New keyword "impure" is introduced to differentiate impure procedural
blocks. All procedural blocks are considered pure by default, unless
"impure" is specified.
-
Procedural blocks can contain any code as defined by the flavor language
as long as it obeys the pure/impure classification.
- We realized impure procedural blocks are not well-defined. Particularly, when assignments to global variables are performed is not well
defined.
- We decided to give-up impure procedural blocks. The 2 requirements that will not be achieved without them are cooperation between assertions and chanign the environemnt.
- We still want to be able to print inside procedural blocks and therefore need to refine the definition of procedural blocks.
Current Proposal for Procedural Blocks
- Procedural blocks will not be triggered on the empty word.
- A special syntax should be defined for attaching a procedural block to a boolean expression.
Procedural blocks attached to a general SERE will be acheived by syntactic sugaring.
- In overlapping operators (fusion and |->) the procedural blocks of the left operand
should be triggered before evaluation of the right operand.
- Procedural blocks can change only local variables and print.
- The syntax for procedural blocks: {SERE}$ procedural block text $
Local Variables
Initial proposal
Proposals for Formal semantics of local variables
Johan's up-to-date proposal can be found here
Dana and Cindy's up-to-date proposal can be found here
Problems found in previous proposals
- Flows in Johan's last proposal:
<<>> is not associatives. s is not equivalent to 's && s' (details are in Johan's email from 28 Nov 06)
- Flows in Dana's previous proposal that can be found here :
Does not handle changes of the local variables on a single letter,
e.g. as may happen with the ":" operator. This produces a disconnection between the semantics of
":" and the semantics of "|->" (details are in Johan's email from 12 Dec 06).
Sanity checks for the formal semantics
- <(),(ab),(),(),...>
|= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {v == 1 || v == -1}
- <(),(ab),(),(),...>
|/= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {v == 1}
- <(),(ab),(),(),...>
|/= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {v == -1}
- <(),(ab),(),(),...>
|= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b ; {v == 1}}!
- <(),(ab),(),(),...>
|= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b ; {v == -1}}!
- <(),(ab),(),(),...> |/=
{{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {true; prev(v==1)}
-
<(),(ab),(),(),...>
|/=
{{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {true; prev(v==-1)}
-
<(),(ab),(),(),...>
|=
{{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {true; prev(v==1 | v== -1)}
Current Proposal for the formal semantics of local variables
Remains to be Done
- Need to revise Proposal A' of the formal semantics to replace the syntax rule for simple local variable assignment by a rule for attaching a general procedural block to a boolean.
-
Formally define triggering of procedural blocks.
- Refine the "pure" requirement to allow printing inside procedural blocks.
LRM Changes
Last updated on 8 Nov 2007.