[Prev][Next][Index][Thread]
specification logic, intuitionistic logic
I had to think a while about your example, and I still do not really
know what to make of it. Here are some of my thoughts:
1) My first thought was that your example is harmless. As you already
said, you are using Strong constancy in this example only for
convenience. You do not want to carry the `global invariant' (that
the array is sorted), through the whole verification of the searching
procedure. The intuistionistic approach allows you to avoid this.
But I suppose that some `syntactic sugar' would do as well---just less
elegantly.
2) On the other hand it's the first example which gives me some
intuition for these non classical rule(s). And I'm getting used to
your intuitionistic way of reasoning about programs.
3) But it seems that you must pay a price. You must `look into' the
commands, e.g. `x:=x+1; x:=x-1' and `skip' have a different
interpretation in your semantics (and they MUST have it, because one
of them interferes with x and the other doesn't). Hence you are far
away from full abstraction (I guess you don't care !).
4) This observation leads me to a general question. Is there a
`natural' contradiction between intuitionistic logic and full
abstraction ? Full abstraction means that two phrases which cannot be
distinguished by a context, are considered as semantically equal.
Sounds `classical' to me. But I don't understand enough of
intuitionistic logic.
Regards, Kurt.
PS: By `state independent formulas' I meant `state independent
assertions (like c>5, where c is a value identifier).