Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199207161349.AA16270@infix.cs.ruu.nl>
Subject: State Logic
To: info-hol@edu.uidaho.cs.ted (hol mailing list)
Date: Thu, 16 Jul 92 15:49:12 METDST

Hi there,

If we are trying to mechanize programing logics, such as Hoare Logic,
it seems that we need to rigorously formalize concepts such as
variables, state, and predicate over states. 

For example if I say 

	x>0 AND y>0

and above to be interpreted as a state predicate (that is a prdecate
over program's states), above should be interpreted as

	!s:STATE. ((s x) > 0) /\ ((s y)>0)

When it comes to HOL unfortunately, all this awful details has to be
written down, plus a handful derivation rules to assist manupulating
state expressions. 

Can anyone perhaps give me some direction to some results about state
predicates? I have the (perhaps not the latest version) result of
Flemming Andersen about UNITY logic, but the state prdicates as
described there was a bit too poor for my purpose. There is also a
work of RJR Back and von Wright: "Refinement Concepts Formalized in
HOL". The state predicate as described there seems to fit well for me,
but I don't know where to get the library.

Thank you kindly,

Wishnu Prasetya
University of Utrecht