# Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

grupos:avispa:denotational_semantics_of_ccp [2009/11/13 11:24]
caolarte
grupos:avispa:denotational_semantics_of_ccp [2011/01/24 15:30] (actual)
Línea 1: Línea 1:
+====== Denotational Semantics for tcc ======
+The semantics of tcc is deﬁned as a function <html>[[·]]</html> which associates to each  process a set of infinite sequences of constraints. We use  C<sup>ω</sup> to denote the set of infinite sequence of constraints in an underlying constraint system.
+
+The semantic equations are described below:
+
+{{ :grupos:avispa:denotation.png |}}
+
+
+ Recall that <html>[[P]]</html> 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
+<html>[[</html>**when** c **do** P <html>]]</html> 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.