Willkommen zum vierten Teil der Artikelserie zum korrekten Programmieren. In Teil 3 hatten wir Liquid Haskell kennen gelernt. Liquid Haskell erlaubt es uns, gewönliche Haskell-Programme zu verifizieren. Im Hintergrund nutzt Liquid Haskell den SMT-Solver Z3, den wir in den Teilen 1 und 2 bereits ausführlich behandelt hatten. Nun ist Haskell bekanntlich eine funktionale Programmiersprache und damit sind wir ohnehin gut aufgestellt, was das fehlerfreie Programmieren angeht. Die Idee von Liquid Haskell lässt sich aber auch auf andere Programmiersprachen übertragen. Mit Verifast gibt es beispielsweise ein Werkzeug, das uns C-Programme auf Korrektheit prüfen lässt.

#include "stdlib.h"

typedef enum { Pulse, NoPulse } Signal;

typedef struct {
    int dx;
    int dy;
    int x;
    int y;
    int d;
    Signal signal;
} Bres;

/*
predicate bres_state(Bres *b, int dx, int dy, int x, int y, int d, Signal s) =
    b->dx     |-> dx            &*&
    b->dy     |-> dy            &*&
    b->x      |-> x             &*&
    b->y      |-> y             &*&
    b->d      |-> d             &*&
    b->signal |-> s             &*&

    // basic bounds/shape
    0 <= dy &*& dy <= dx &*&    // Note: both dy == 0 and dy == dx edge cases are indeed fine
    0 <= x &*&                  // follows from initial state and x_i == x_(i-1) + 1
    0 <= y &*&                  // follows from initial state and y_i == y_(i-1) || y_i == y_(i-1) + 1
    y <= dy &*&                 // y never overshoots dy

    // "Bresenham" invariant of d
    d == 2*dy*x - 2*dx*y + 2*dy - dx &*&

    // Pixel correctness invariant: 2*dx*y - dx <= 2*dy*x <= 2*dx*y + dx
    -dx <= err(dx, dy, x, y) &*& err(dx, dy, x, y) < dx
;
*/

void step(Bres *b)
{
    if (b->d >= 0) {
        b->x += 1;
        b->y += 1;
        b->d += (2 * b->dy) - (2 * b->dx);
        b->signal = NoPulse;
    } else {
        b->x += 1;
        b->d += 2 * b->dy;
        b->signal = Pulse;
    }
}

void step(Bres *b)
    //@ requires bres_state(b, ?dx, ?dy, ?x, ?y, ?d, _) &*& x < dx;
    //@ ensures bres_state(b, dx, dy, x+1, _, _, _);
{
    //@ open bres_state(b, _, _, _, _, _, _);
    if (b->d >= 0) {
        b->x += 1;
        b->y += 1;
        b->d += (2 * b->dy) - (2 * b->dx);
        b->signal = NoPulse;
        //@ bres_NE_implies_y_lt_dy(dx, dy, x, y, d); // y < dy
        //@ close bres_state(b, _, _, x+1, y+1, _, NoPulse);
    } else {
        b->x += 1;
        b->d += 2 * b->dy;
        b->signal = Pulse;
        //@ close bres_state(b, _, _, x+1, y, _, Pulse);
    }
}