|
Recent I proved Hoare's Axiom system about the
verification of
program correctnesss,using Mizar's scheme. As
far as I know,nobody
proved it by natural language,because it is
difficult to describe
proof step rigorously by natural language. In
this sense,Formal
language such as Mizar is very
good.
I think Mizar's scheme form is to describe
the high order logic problem,
while Mizar's theorem form is to describe the
first order logic problem.
Hoare's Axiom system is a high order logic
problem,so I must use Mizar's
scheme to describe it.However, I found several
scheme form is not
available. I guess this may be a Mizar's
bug.
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: .....
If we cite this scheme by form "from
HoareRule(C1,C2,C3)", error 23
occurs. error 23 is Impossible reconstruction of
the definiens of
a predicate.
When I change the above definition into
following form,no error occrs.
scheme HoareRule{ F(set)->
Nat,P[set],...}:
F(x)=F(x) & (P[x] or not
P[x])
Q[F(g(x))] &
P[g(x)]
provided C1: R[F(...)]
C2: P[x]
C3: ..... This definition is completely the same as the previous definition,but not natrual, because conclusion F(x)=F(x) &
(P[x] or not P[x]) is
redundant.
JingChao Chen
|