• Parcialna pravilnost
• Totalna pravilnost
• Primeri dokazov

Parcialna pravilnost

Zančna invarianta

if()                   P1(y)   P2(y)
 { }  //P1(y);           |       |
else                     |<------'
 { }  //P2 (y);          |
//P1(Y) v P2(Y)        P1(y)||P2(y)

Če nam dokazovnje uspe z zančno invarianto smo dokazali pravilnost programa.

Totalna pravilnost

Problematične so zanke.

• Za vsako zanko v programu definiramo zančno spremenljivko l (naravno število, ki se zmanjšuje ob vsaki iteraciji)
• Potrebujemo dobro utemeljeno množico D

utemeljena množica je množica, ki je delno urejena in nima neskončnih padajočih zaporedij

• l in D morata biti tako defnirani da lahko definiramo še zančno invarianto:

l pred izvajanjem

ll po izvajanju

l > ll

Primeri

Izračun faktoriele

static public int faks(int n) {
  int i=0; //stevec
  int f=1; //vrednost faktoriele 
  while (i<n) {
    i++;  //povečamo števec
    f*=i; //množimo s prejšnjo vrednostjo
  }
  return f; //vrnemo rezultat
}

Postavimo zančno invarianto (označeno z I), ki velja v točkah označenih z *:

     
     |    
   i <- 0
     |
     | i=0
     |
     *
     |
     | f=1 && i=0 => [f=i!]
     |
     |<------*------------------------.  f/i = (i-1)!
     *                                |  f= i×(i-1)! = i! && (i ≤ n)
     |                                |
   f <- 1                             |
     |       yes                      |
     |                                |
     |       .-(f=i!)&&(i<n)   .-(f=(i-1)!)&&(i-1<n) = i ≤ 0
     |       |                 |      |
   [i < n]---*----  i <- i+1  --- f <- f*i
     |
     * no
     |
     | f=n! => f=i!
     | 
     |
   faks<- f
     |    
     

zančna spremenljivka

zančna invarianta

static public int faks(int n) {
  int i=0; //stevec
  int f=1; //vrednost faktoriele
  
  while (i<n) {
    
    i++;  //povečamo števec
    f*=i; //množimo s prejšnjo vrednostjo
    
  }
  
  return f; //vrnemo rezultat
}

Množenje z inkrementom

static public int prod (int x, int y) {
  <math>\! \Phi (x,y) = (x,y \in \mathbb{N}_0)</math>
  int i,j,p; //stevca, vmesni rezultat
  i = 0;
  p = 0; //init
  while ( i! = x ) {
    while ( j! = y ) {
      p++;
      j++;
    }
    i++;
  }
  return p;
  <math>\! \Psi (prod, x, y) = (prod = x \cdot y)</math>
}

     
   |
 i <- 0   
   |      
 f <- 0   
   |
   *  
   | 
   |<-----*---------------------------------------------------.
   |                        .--------*---------------.        |
   |                        |                        |        |
   |                        |                     j <- j+1    |
   |   yes                  v             yes        |        |
 i ≠ 0 --*-------  j<-0 --*---*-- j ≠ y ---*----  p <- p+1    |
   |                                |                         |
   * no  p=i×j                      * no                      |
   |                                |                         |
  prod<-p                           `------------ i<-i+1 -----´
   |
   | prod = x×y
      

(notranja zanka)

(zunanja zanka)

750px