On 22 Sep 2012, at 00:11, Jon Lockhart wrote:

> Roger,
> I tried what you mentioned after Phil brought it up and if you try to do 
> State' and then push' = {} the system throws an error saying "No free types 
> allowed in predicates" which to me means that push is not accessible in the 
> predicate section.

I don't recognise that error message. Is your state variable called "push" or 
something a little different? Please try again and report back if you really 
can't get things to work.

> I also agree that doing the precondition seems redundant now after you 
> explain things, b/c since they are not operators so far, there have been no 
> way to show there were correct unless specifying everything that was in the 
> paragraph, as there was nothing changing, i.e. having a prime after it.
> So ProofPower won't let me use the 2 prime idea, so that must mean it is not 
> in the ISO Standard as good practice. 

I am not quite sure what you mean. ProofPower and the ISO Standard don't impose 
any conventions on how you use schemas to specify a system. If you want to use 
the style where initialisation schemas specify an after-state (with primes), 
then you may.



Proofpower mailing list

Reply via email to