Denotational Semantics for tcc

The semantics of tcc is deﬁned as a function [[·]] which associates to each process a set of infinite sequences of constraints. We use Cω to denote the set of infinite sequence of constraints in an underlying constraint system.

The semantic equations are described below:

Recall that [[P]] aims at capturing the strongest postcondition (or quiescent sequences) of a process P. So, skip cannot add any information to any sequence (Equation DSkip). The sequences to which tell ( c ) cannot add information are those whose first element entails c (Equation DTell). A sequence s is in [[when c do P ]] if either s(1) cannot entail the guard c or s(1) entails c and is quiescent for Q (Equation DAsk). A sequence is quiescent for P || Q if it is for P and Q (Equation DPar).

The process next P has no influence on the first element of a sequence, thus d.s is quiescent for it if s is quiescent for P (Equation DNext). A similar explanation can be given for the process unless c next P (Equation DUnl). A sequence s is quiescent for !P if every suffix of s is quiescent for P (Equation DRep).

We say that s is an x-variant of s' if ∃x.s(i)=∃x.s'(i) for i>0 (i.e. s and s' differ only on the information about x). A sequence s is quiescent for Q=(local x;c )P if there exists an x-variant s' of s s.t. s' is quiescent for P and s'(1) entails c. Hence, if P cannot add any information to s' then Q cannot add any information to s.

grupos/avispa/denotational_semantics_of_ccp.txt · Última modificación: 2011/01/24 15:30 (editor externo) 