Vi slutter denne lektion af med et kapitel om programkorrekthed.

15.1 Assertions

 

15.1.  Assertions
Indhold   Op Forrige Næste   Slide Aggregerede slides    Stikord Programindeks Opgaveindeks 

Ved brug af logiske udtryk kan vi ofte få et program til at checke sig selv. Vi kalder ofte sådanne udtryk for assertions. Hvis et assertion beregnes til false (altså 0 i C) stoppes programmet med en informativ besked om, hvad der er galt.

To specielt interessante assertions: Præbetingelse af en funktion: Fortæller om det giver mening at kalde funktionen Postbetingelse af en funktion: Fortæller om funktionen returnerer et korrekt resultat

Vi illustrerer ideen om assertions med en forkert og en korrekt implementation af en kvadratrodsfunktion. Først, i program 15.2, en underlig og meget forkert implementation af my_sqrt som blot returnerer konstanten 7.3 uanset input.

Den røde prebetingelse i program 15.1 udtrykker, at parameteren til my_sqrt skal være ikke-negativ. Den blå postbetingelse udtrykker, at kvadratet af resultatet, altså res², skal være meget tæt på det oprindelige input x. Vi kan ikke forvente at ramme x eksakt, idet der jo altid vil være risiko for afrundingsfejl når vi arbejder med reelle tal på en computer.

Med den viste implementation af my_sqrt vil postbetingelsen (den blå assertion) fejle for de fleste input.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

#include <stdio.h>
#include <math.h>
/* #define NDEBUG 1 */
#include <assert.h>

int isSmallNumber(double x){
  return (fabs(x) < 0.0000001);
}   

double my_sqrt(double x){
  double res;
  assert(x >= 0);
  res = 7.3;
  assert(isSmallNumber(res*res - x));
  return res;
}

int main(void) {

  printf("my_sqrt(15.0): %lf\n", my_sqrt(15.0));
  printf("my_sqrt(20.0): %lf\n", my_sqrt(20.0));
  printf("my_sqrt(2.0): %lf\n", my_sqrt(2.0));
  printf("my_sqrt(16.0): %lf\n", my_sqrt(16.0));
  printf("my_sqrt(-3.0): %lf\n", my_sqrt(-3.0));
  
  return 0;
}

Den udkommenterede konstant NDEBUG kan bruges til at styre, om assertions rent faktisk eftercheckes. Hvis kommentarerne fjernes, vil assertions ikke blive beregnet.

Lad os også vise en korrekt implementation af en kvadratrodsfunktion. Vi benytter rodsøgningsprogrammet fra afsnit 13.2 til formålet. Den centrale observation er, at vi kan finde kvadratroden af k ved at finde en rod i funktionen f(x) = x² - k i intervallet 0 og k. Det er nøjagtigt hvad vi gør i program 15.2 .

Bemærk de røde og blå dele i program 15.2, som er hhv. prebetingelse og postbetingelse af my_sqrt, ganske som i den forkerte udgave af kvadratrodsfunktionen i program 15.1. Den lilla del er funktionen f, som vi diskuterede ovenfor.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

#include <stdio.h>
#include <math.h>
/* #define NDEBUG 1 */
#include <assert.h>

int isSmallNumber(double x){
  return (fabs(x) < 0.0000001);
}   

double displacement; 

double f (double x){
  return (x * x - displacement);
}

int sameSign(double x, double y){
  return x * y > 0.0;
}

double middleOf(double x, double y){
  return x + (y - x)/2;
}

double findRootBetween(double l, double u){
 while (!isSmallNumber(f(middleOf(l,u)))){ 
   if(sameSign(f(middleOf(l,u)), f(u)))
     u = middleOf(l,u);
   else 
     l = middleOf(l,u);
 }
 return middleOf(l,u);
}  


double my_sqrt(double x){
  double res;
  assert(x >= 0);
  displacement = x; 
  res = findRootBetween(0,x);
  assert(isSmallNumber(res*res - x));
  return res;
}

int main(void) {

  printf("my_sqrt(15.0): %lf\n", my_sqrt(15.0));
  printf("my_sqrt(20.0): %lf\n", my_sqrt(20.0));
  printf("my_sqrt(2.0): %lf\n", my_sqrt(2.0));
  printf("my_sqrt(16.0): %lf\n", my_sqrt(16.0));
  
  return 0;
}

Vi kan også illustrere assertions i selve rodsøgningsfunktionen findRootBetween, som oprindelig blev vist i program 13.1. Dette er illustreret i program 15.3 herunder.

I den røde prebetingelse af findRootBetween udtrykker vi at l skal være mindre end eller lige med u og at fortegnet af f(l) og f(u) skal være forskellige. I den blå postbetingelse kræver vi at f(res) er meget tæt på 0. Dette udtrykker at funktionen findRootBetween er korrekt på de givne input.

1
2
3
4
5
6
7
8
9
10
11
12
13

double findRootBetween(double l, double u){
 double res;
 assert(l <= u); assert(!sameSign(f(l), f(u))); 
 while (!isSmallNumber(f(middleOf(l,u)))){ 
   if(sameSign(f(middleOf(l,u)), f(u)))
     u = middleOf(l,u);
   else 
     l = middleOf(l,u);
 }
 res = middleOf(l,u);
 assert(isSmallNumber(f(res)));
 return res;
}