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

*To*: Kun Wei <k.wei@eim.surrey.ac.uk>*Subject*: Re: about prove commands!*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Fri, 19 Sep 2003 10:10:09 -0700*CC*: pvs-help@csl.sri.com*In-Reply-To*: <169428233000.20030917142706@surrey.ac.uk>*References*: <169428233000.20030917142706@surrey.ac.uk>*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3.1) Gecko/20030425

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

**References**:**about prove commands!***From:*Kun Wei <k.wei@eim.surrey.ac.uk>

- Prev by Date:
**about prove commands!** - Next by Date:
**PVS/Cygwin** - Prev by thread:
**about prove commands!** - Next by thread:
**PVS installation with redhat Linux 9** - Index(es):