3.15 Problem: Contracts
Design a reduction semantics (standard or regular) for a
Lambda language with contracts. Here is the syntax:
(define-language Lambda (e ::= x (lambda (x) e) (e e) n (+ e e) (if0 e e e) (c · e x x) (blame x)) (n ::= number) (c ::= num? even? odd? pos? (c -> c)) (x ::= variable-not-otherwise-mentioned))
The contract primitives are interpreted as follows:
The contract form (c · e x_s x_c) checks contract c on
e. If e breaks the contract, the semantics signals a
(blame x_s) error; other contract violations signal a
(blame x_c) error.
Consider these three examples where the same contracted function works
well, is blamed, or blames its context depending on the argument:
(define a-module (term {(even? -> pos?) · (lambda (x) (+ x 1)) server client})) (define p-good (term [,a-module 2])) (define p-bad-server (term [,a-module -2])) (define p-bad-client (term [,a-module 1]))
Work through the examples by hand to find out why the three programs work
fine, blame the server, and blame the client for contract violations,
respectively.