Hello Amira, I am not sure I understand your question. The canonical way for hiding an internal variable x from a specification is existential quantification: Internal == ... \* specification involving x and y Spec == \EE x : Internal A behavior (i.e., a sequence of states) satisfies Spec if there is a way to assign suitable values to x at every state such that the resulting behavior satisfies Internal. (The fine print is explained for example in chapters 4 and 8.8 of "Specifying Systems".) Perhaps your question is how one can verify properties of a specification involving such quantifiers? Neither TLC nor TLAPS currently support quantification over state variables. In order to prove properties of Spec above, note that Spec => Property holds if and only if Internal => Property holds (this is just an application of a standard quantifier rule), so you may just as well use the formula without the quantifier. In order to prove refinement of Spec, i.e. verify Implementation => Spec for some formula Implementation that represents a lower-level implementation of your specification, the standard approach is to use a refinement mapping: define a state function ximpl == ... \* defined in terms of the variables of formula Implementation such that you have Implementation => Internal[ximpl / x] where the latter denotes formula Internal with x substituted by ximpl. TLA+ does not have explicit syntax for substitution, so you'll write something like (in the module containing formula Implementation, and assuming that formula Internal appears in a module called Highlevel) HL == INSTANCE Highlevel WITH x <- ximpl then check (using for example TLC) that you have the implementation Implementation => HL!Internal I recommend that you also look at sections 6.6ff. or sections 8.4ff. of the hyperbook. Hope this helps, Stephan On 06 Jul 2014, at 13:45, Amira Methni <methni...@xxxxxxxxx> wrote:
|