Racket

Lackadaisical Contracts🔗ℹ

Cameron Moy

(require lackadaisical-contract)
	package: lackadaisical-contract-lib

This library provides contract forms that implement the lackadaisical checking strategy. In lackadaisical, interactions with higher-order values at the contract level are deferred until the program itself exhibits those same interactions.

syntax
(->l ([dom-id dom-expr] ...) pre [cod-id cod-expr] post)

pre =
| #:pre (id ...) expr pre

post =
| #:post (id ...) expr post

This contract form is similar to ->* except it implements lackadaisical checking for preconditions and postconditions that depend on higher-order values.

> (define/contract (bad g)
    (->l ([g (-> integer? integer?)])
         #:pre (g) (zero? (g 1))
         [result integer?])
    (g 1))
> (bad values)
bad: contract violation
  failed clause (#:pre (g) (zero? (g 1)))
  in: (->l
       ((g (-> integer? integer?)))
       #:pre
       (g)
       (zero? (g 1))
       (result integer?))
  contract from: (function bad)
  blaming: top-level
   (assuming the contract is correct)
  at: eval:1:0
> (define/contract (ok g)
    (->l ([g (-> integer? integer?)])
         #:pre (g) (zero? (g 1))
         [result integer?])
    (g 17))
> (ok values)
17

Notice that the precondition does not fail for ok because its body does not actually apply g to 1. While the precondition fails for bad because it can observe the result of (g 1) and witness that it is not actually 0.

syntax
(self/c id ([set-id set-ctc] ...) body clause ...)

clause = (∀ ([id dom] ...) prop-expr ...+)

The self/c contract expresses declarative properties of a function via universal quantification. This kind of specification is helpful for stating mathematical properties in their most natural form. Here is an example of injectivity as a contract:

> (define injective/c
    (self/c f ([A any/c])
      (-> A any/c)
      (∀ ([x A] [y A])
        (implies (equal? (f x) (f y))
                 (equal? x y)))))
> (define/contract (floor* x)
    injective/c
    (floor x))
> (floor* 3.5)
3.0
> (floor* 4.5)
4.0
> (floor* 4.85)
floor*: broke its own contract
  promised: (implies (equal? (f x) (f y)) (equal? x y))
  where: x is 4.5, y is 4.85
  in: (self/c
       f
       ((A any/c))
       (-> A any/c)
       (∀
        ((x A) (y A))
        (implies
         (equal? (f x) (f y))
         (equal? x y))))
  contract from: (function floor*)
  blaming: (function floor*)
   (assuming the contract is correct)
  at: eval:6:0

This contract uses lackadaisical checking, in the sense that interactions with f in the body of universally-quantified expressions are not evaluated immediately.