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.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
