MIZAR言語で矛盾がなければプログラム上のバグが無くなる。
 C言語では                  論理記号             MIZAR言語 
for(int x=0;x(∀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∈自然数,idefinition 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;
---------------------------------------------------------------------------------------
  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];
  }
  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 (x^2 = 1 implies x=1 or x=-1) implies (x^3 = 1 & x^2 =1 implies x=1 or x=-1)
--------------------------------------------------------------------------------------
  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;    ::証明終了