[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: about prove commands!



Kun Wei wrote:
> Hello,
> 
> I got a big problem when I proved the following lemma. Because I don't
> know too much prover commands, who could give me any suggestions.
> That's so appreciated!
> 
> 
> hide_para.1.2 :
> 
> [-1]  P2!1(t1!3)
> [-2]  P1!1(t1!2)
> [-3]  t1!1 = leak(t1!2, X!1)
> [-4]  t2!1 = leak(t1!3, X!1)
> {-5}  prod(A!1)(leak(t1!2, X!1), leak(t1!3, X!1), x!1)
> [-6]  disjoint?(A!1, X!1)
>   |-------
> [1]   EXISTS (t1_1:
>                 ({t: trace[E] |
>                     EXISTS (t1: (P1!1), t2: (P2!1)):
>                       prod(A!1)(t1, t2, t)})):
>         x!1 = leak(t1_1, X!1)
> 
> ====================================================
> ps: Here prod is a function in which t is observed as a result if t1
> and t2 can be executed concurrently by two processes which synchronise
> on A. Indeed, t,t1 and t2 are traces denoted as lists.
> 
> 
> prod(A)(t1, t2, t) : RECURSIVE bool =
>     CASES t OF 
>         null : null?(t1) AND null?(t2),
>         cons(x, y) :
>           IF A(x)
>           THEN  
>                 cons?(t1) AND cons?(t2) AND
>                 car(t1) = x AND car(t2) = x
>                 AND prod(A)(cdr(t1), cdr(t2), y)
>           ELSE 
>                 (cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y)) 
>              OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y))
>           ENDIF
>     ENDCASES
>   MEASURE length(t)
> 
> 
> leak(t,A) is a function that gets rid of t's events included in set A
> for example:
> 
>  t: a->b->c-> Stop
>  A:{a,b}
>  leak(t,A)= c->Stop
> 
> 
> ok, let's go back the above question. In 1.2, I can't use inst?
> because I can't find a instance.  Please suggest me some commands to
> make the prove carry on.
> 
> Many thanks!
> 
> Kun Wei
> 

Hi,

The above goal looks like a dead end. What you have to do
is prove your property by induction.

Assuming you have defined a CSP hide operator as follows

   hide(P, X): process = { t | EXISTS (t1: (P)): t1 = leak(t, X) }

It seems that you're trying to prove something close to:

   disjoint(A, X) => subset?(hide(Par(A)(P1, P2), X),
                             Par(A)(hide(P1, X), hide(P2, X)))

After a few steps, you should get to a goal like:

   {-1} disjoint(A!1, X!1)
     |------------
   {1} FORALL x: hide(Par(A!1)(P1!1, P2!1), X!1)(x) IMPLIES
                       Par(A!1)(hide(P1!1, X!1), hide(P2!1, X!1))(x)

Then try to use induction on "x" at that point.

Bruno
-- 
Bruno Dutertre                             | bruno@sdl.sri.com
SDL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717