# A Fairly Simple VC Generator for Hoare Logic

**URL:** <https://racket.discourse.group/t/a-fairly-simple-vc-generator-for-hoare-logic/4391>\
**Category:** Show & Tell\
**Created:** [September 18, 2026, 12:16pm UTC](https://racket.discourse.group/t/a-fairly-simple-vc-generator-for-hoare-logic/4391 "2026-09-18T12:16:21Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![ulambda](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ulambda/32/1495_2.png) [@ulambda](https://racket.discourse.group/u/ulambda)\
**Post date:** [September 18, 2026, 12:16pm UTC](https://racket.discourse.group/t/a-fairly-simple-vc-generator-for-hoare-logic/4391/1 "2026-09-18T12:16:21Z")

</div>

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

```scheme
(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.

```scheme
> (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))))

```

```scheme
> (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.