Mizar/他言語との比較

出典: フリー教科書『ウィキブックス(Wikibooks)』
ナビゲーションに移動 検索に移動
MIZAR言語で矛盾がなければプログラム上のバグが無くなる。
C言語では 論理記号 MIZAR言語
for(int x=0;x<MAX;x++){A} (∀x∈NAT 0≦x≦MAX)(A)for x being Nat st x< MAX holds A
if(A){B}else{C} (A⇒B)and(not A⇒C) (A implies B)&(!A implies C)
int y; (∃y∈整数) ex y being INT
int y[MAX_N]; ∀i∈自然数,i<MAX_N,∃yi∈整数 definition let y be XFinSequence of INT,n be Integer; assume A1: 0< n & n< len a;
int f(int a){} ∃a∈整数 f(a) definition let a be Integer; func f(a) -> Integer means :ラベル:

 switch(x)
 {
 case 1:
       break;
 case 2:
       break;
 default:
 
 }
 L:(x=1 or x=2 or not(x=1 & x=2))
 now per cases by L;
   case LA:x=1;
   case LB:x=2;
   case LC:not (x=1 & x=2);
 end;

C言語で処理
 int sumarray_prg(int a[MAX_N],int n)
 {
  int s[MAX_N],i;
  if (!(0< n && n< MAX_N))return -1;
  s[0]=0;
  for (i=0;i< n;i++)
   { s[i+1]= s [i] + a[i+1];
   } 
  return s[n];
 }
mizarで処理
 definition let a be XFinSequence of INT,n be Integer;
  assume A1: 0<  n & n< len a;
   func sumarray_prg(a,n) -> Integer means
   :SS00: ex s being XFinSequence of INT st s.0=0 &
  (for i being Nat st i< n holds s.(i+1)=s.i +a.(i+1))
       & it=s.n;
  existence;
  uniqueness;
 end;

命題:仮想定理: ...⇒***
theorem ... implies ***
 theorem (x^2 = 1 implies x=1 or x=-1) implies (x^3 = 1 & x^2 =1 implies x=1 or x=-1)

証明
assume p; : p を仮定する
 proof assume A1: (x^2 = 1 implies x=1 or x=-1);
 thus x^3 = 1 & x^2 =1 implies x=1 or x=-1
   proof assume x^3 = 1 & x^2 =1;
         :: then  直前の式から
         :: thus q;     : q が示せた
         :: hence は then + thus になっています
         hence x=1 or x=-1 by A1;
   end;
 end;    ::証明終了
then :直前の式より
thus q; :結論としてq が示せた
hence q; :(then + thus)直前の式より、結論としてq が示せた
矛盾(間違え) : contradiction
無矛盾(正解) : not contradiction