A Fairly Simple VC Generator for Hoare Logic

Show & Tell
1

I wrote a fairly simple verification condition generator in less than 30 lines.

(define (subst Q E V)
  (cond ((pair? Q) (cons (subst (car Q) E V)
                         (subst (cdr Q) E V)))
        ((eq? Q V) E)
        (else Q)))
(define (:= V E)
  (case-lambda
    ((P Q) (list `(=> ,P ,(subst Q E V))))
    ((Q) (values (subst Q E V) '()))))
(define ((IF S C1 C2) P Q)
  (append (C1 `(and ,P ,S) Q)
          (C2 `(and ,P (not ,S)) Q)))
(define ((WHILE S R C) P Q)
  `((=> ,P ,R)
    (=> (and ,R (not ,S)) ,Q)
    . ,(C `(and ,R ,S) R)))
(define ((PRE R C) Q)
  (values R (C R Q)))
(define ((SEQ C . C*) P Q)
  (let iter ((RC* (reverse C*))
             (R Q) (VC '()))
    (if (null? RC*)
        (append (C P R) VC)
        (let-values (((R VC0) ((car RC*) R)))
          (iter (cdr RC*) R (append VC0 VC))))))
(define (Hoare P C Q) (C P Q))

And here are some examples.

> (Hoare
   '(and (= X x) (= Y y))
   (SEQ (:= 'R 'X)
        (:= 'X 'Y)
        (:= 'Y 'R))
   '(and (= Y x) (= X y)))
'((=> (and (= X x) (= Y y)) (and (= X x) (= Y y))))

> (Hoare
   #t
   (SEQ (:= 'R 'X)
        (:= 'Q 0)
        (PRE
         '(and (= R X) (= Q 0))
         (WHILE '(<= Y R)
                '(= X (+ R (* Y Q)))
                (SEQ (:= 'R '(- R Y))
                     (:= 'Q '(+ Q 1))))))
   '(and (= X (+ R (* Y Q))) (< R Y)))
'((=> #t (and (= X X) (= 0 0)))
  (=> (and (= R X) (= Q 0)) (= X (+ R (* Y Q))))
  (=> (and (= X (+ R (* Y Q))) (not (<= Y R))) (and (= X (+ R (* Y Q))) (< R Y)))
  (=> (and (= X (+ R (* Y Q))) (<= Y R)) (= X (+ (- R Y) (* Y (+ Q 1))))))

I hope you can have fun with it.

4 Likes