Mizar/他言語との比較

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