Menu
▾
▴
Re: [Hol-info] Help setting up goal
|
From: Ewa R. <ewu...@ho...> - 2007-04-21 17:19:41
|
John,
=20
This tip was terrific, I was able to define choice and also prove the the u=
nconditional and weak fairness.
Here is what I did:
=20
let choice =3D new_definition `Choice (c1:(S->bool)->(S->bool)) (c2:(S->boo=
l)->(S->bool)) q =3D {s| c1 q s \/ c2 q s}`;;
let monotonic =3D new_definition `monotonic c <=3D> !q q=92. q SUBSET q=92 =
=3D=3D> (c q) SUBSET (c q=92)`;;
=20
I proved the monotonicity:
=20
`monotonic c1 /\ monotonic c2 =3D=3D> monotonic (Choice c1 c2)`,
=20
For unconditionally fair I put: (I narrowed down choice for two if statemen=
ts only, which should be ok for my project)
=20
`monotonic (If e1 c1) /\ monotonic (If e2 c2) /\ correct p (If e1 c1) q /\ =
correct p (If e2 c2) q /\ (!X:int. correct (\s. X=3Ds) (If e1 c1) (\s. s<=
=3DX)) /\ (!X:int. correct (\s. X=3Ds) (If e2 c2) (\s. s<=3DX)) =3D=3D> co=
rrect p (Choice (If e1 c1) (If e2 c2)) q`
=20
and for weak fairness I was able to write:
=20
`monotonic (If e1 c1) /\ monotonic (If e2 c2) /\ correct p (If e1 c1) q /\ =
correct p (If e2 c2) q /\ (!X:int. correct (\s. X=3Ds) (If e1 c1) (\s. s<=
=3DX)) /\ (!X:int. correct (\s. X=3Ds) (If e2 c2) (\s. s<=3DX)) /\((!X:int.=
correct (\s. X=3Ds) (If e1 c1) (\s. s<X)) \/ (!X:int. correct (\s. X=3Ds) =
(If e2 c2) (\s. s<X)))=3D=3D> correct p (Choice (If e1 c1) (If e2 c2)) q`
=20
which is exactly what I wanted to achieve.
=20
I'm trying now to prove a simple example of random number generator:
=20
b:=3Dtrue, x:=3D0;
while (b){
If b x:=3Dx+1;
If b b:=3Dfalse;
}
=20
I set the goal to be:
=20
g `correct (\(b,x). T) ( Assign (\(b,x). 1,0) ;; assert (\(b,x). b =3D=
1 /\ x =3D 0) ;; While (\(b,x). b =3D 1) ( assert (\(b,x). b > 0) ;; =
variant (measure (\(b,x). b =3D 1)) ;; =
Choice (If (\(b,x). b =3D 1) (Assign (\(b,x). b,x + 1))) =
(If (\(b,x). b =3D 1) (Assign (\(b,x). 0,x)))) ;; =
assert (\(b,x). b=3D0 /\ ~(x<0))) (\(b,x). b=3D0)`;;
=20
and I get error: Types cannot be unified.
=20
I replaced all \(b,x) with \(b:int,x:int) and I get the same message.
I cannot find a reason for this. Any clue?
=20
Thank you
Ewa
=20
=20
=20
=20
=20
=20
> To: ewu...@ho...> CC: hol...@li...> Subject: Re=
: [Hol-info] Help setting up goal> Date: Fri, 20 Apr 2007 04:40:22 +0100> F=
rom: Joh...@cl...> > > Hi Ewa,> > | The exact definition of c=
hoice would say:> |> | for any p (c1 || c2) q either p c1 q or p c2 q is ex=
ecuted. Thus the> | state after execution would be either c1 q or c2 q if b=
oth guards for c1> | and c2 hold.> > Ah, sorry, I'd mistakenly assumed that=
you were using weakest> preconditions, not initial/final state relations. =
So I guess the> appropriate definition would just be something like> > let =
choice =3D new_definition `(c1 || c2) s t <=3D> c1 s t \/ c2 s t`;;> > to i=
ndicate that the choice can lead from an initial state "s" to a> final outc=
ome "t" if and only if either or both of the component> commands can.> > | =
What I'm trying to accomplish here is formalization of fairness for> | nond=
eterministic loops (For example where e1 and e2 are both true on each> | it=
eration). I'm trying to follow the definitions of fairness specified in> | =
Nassim Francez book "Fairness".> > I took a quick glance at the book. It se=
ems that the "micro" semantics> of commands there is indeed as relations be=
tween initial and final> states (or outcomes, adding an extra "fail" state)=
. I'm wondering if> you will also need to formalize the notion of the label=
led tree of> computation sequences on page 10. Or can you do what you want =
purely> in terms of the basic relational semantics?> > John.
_________________________________________________________________
Connect to the next generation of MSN Messenger=A0
http://imagine-msn.com/messenger/launch80/default.aspx?locale=3Den-us&sourc=
e=3Dwlmailtagline=
|
