Re: Mizar's scheme is very useful but maybe have a bug

["CHENJINGCHAO" <chen-jc@cs.sjtu.edu.cn>]

>On Fri, 21 Apr 2000, CHENJINGCHAO wrote:
>> For example,we can define the following scheme:
>> 
>>  scheme HoareRule{ F(set)-> Nat,P[set],...}:
>>     Q[F(g(x))] & P[g(x)]
>> provided
>> C1:  R[F(...)]
>> C2:  P[x] 
>> C3:  .....
Andrzej wrote:

>In your example (I do not know what C3 is) the problem might be with Q
>(a part of the definition of F() might be incorporated) or with R (the
>same)
>From my observation, the problem was not with Q or with R. It
seems to be related to g(x). The reason is  that g(x) is not a simple
parameter for F() or P[].   


>Could you send us the complete example.

The following is a  realistic  example I met when proving the 
correctness of a program.
-------
scheme WhileResult{ F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[set]}:
   F(s())=F(s()) & (P[s()] or not P[s()]) &
   F(Dstate IExec(while<0(a(),i(),I()),s()))=0 &
   P[Dstate IExec(while<0(a(),i(),I()),s())]
provided
C1: card I() > 0 and
C2: for t be State of SCMPDS st P[Dstate t] holds
      F(Dstate(t))=0 iff t.DataLoc(s().a(),i()) ?0 and
C3: P[Dstate s()] and
C4: for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) < 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))]

Where Function Dstate is defined as follows:
definition
 let t be State of SCMPDS;
 func Dstate(t) -> State of SCMPDS means
:Def01: 
  for x be Any
   holds (x is element of SCM-Data-Loc implies it.x = t.x)
   & ( x is element of the Instruction-Locations of SCMPDS implies
   it.x = goto 0) &  (x=IC SCMPDS implies it.x=inspos 0);
end

---------
The article including the above example will be sent to
MML soon.

Regards,


JingChao Chen
Shanghai,China