Racket程式設計指南——7 合約

7 合約

本章對Racket的合約系統提供了一個詳細的介紹。

在《Racket參考》中的“合約（Contracts）”部分提供有對合約更詳細的資訊。

7.1 合約和邊界

7.1.1 合約的違反

7.1.2 合約與子產品的測試

7.1.3 嵌套合約邊界測試

7.2 函數的簡單合約

7.2.1 ->類型

7.2.2 使用define/contract和 ->

7.2.3 any和any/c

7.2.4 運轉你自己的合約

7.2.5 高階函數的合約

7.2.6 帶”???“的合約資訊

7.2.7 解析一個合約錯誤資訊

7.3 一般功能合約

7.3.1 可選參數

7.3.2 剩餘參數

7.3.3 關鍵字參數

7.3.4 可選關鍵字參數

7.3.5 case-lambda的合約

7.3.6 參數和結果依賴

7.3.7 檢查狀态變化

7.3.8 多個結果值

7.3.9 固定但靜态未知數量

7.4 合約：一個完整的例子

7.5 結構上的合約

7.5.1 確定一個特定值

7.5.2 確定所有值

7.5.3 檢查資料結構的特性

7.6 用#:exists和#:∃抽象合約

7.7 附加執行個體

7.7.1 一個客戶管理器組建

7.7.2 一個參數化（簡單）棧

7.7.3 一個字典

7.7.4 一個隊列

7.8 建立新合約

7.8.1 合約結構屬性

7.8.2 使所有警告和報警一緻

7.9 問題

7.9.1 合約和eq?

7.9.2 合約邊界和define/contract

7.9.3 存在的合約和判斷

7.9.4 定義遞歸合約

7.9.5 混合set!和contract-out

7.1 合約和邊界

如同兩個商業夥伴之間的一個合約，一個軟體合約是雙方之間的一個協定。這個協定規定了從一方傳給另一方的每一”産品“（或值）的義務和保證。

是以，一個合約确定了雙方之間的一個邊界。每當一個值跨越這個邊界，這個合約監督系統執行合約檢查，確定合作夥伴遵守既定合約。

在這種精神下，Racket主要在子產品邊界支援合約。具體來說，程式員可以附加合約到provide從句進而對輸出值的使用施加限制和承諾。例如，輸出描述

#lang racket

(provide (contract-out [amount positive?]))

(define amount ...)

對上述amount值的子產品的所有用戶端的承諾将始終是一個正數。合約系統仔細地監測了該子產品的義務。每次一個用戶端引用amount時，螢幕檢查amount值是否确實是一個正數。

合約庫是建立在Racket語言中内部的，但是如果你希望使用racket/base，你可以像這樣明确地輸入合約庫：

#lang racket/base

(require racket/contract) ; 現在我們可以寫合約了。

(provide (contract-out [amount positive?]))

(define amount ...)

7.1.1 合約的違反

如果我們把amount綁定到一個非正的數字上，

#lang racket

(provide (contract-out [amount positive?]))

(define amount 0)

那麼，當子產品被需要時，監控系統發出一個合同違反的信号并将違背承諾歸咎于這個子產品。

一個更大的錯誤将是綁定amount到一個非數字值上：

#lang racket

(provide (contract-out [amount positive?]))

(define amount 'amount)

在這種情況下，監控系統将應用positive?到一個符号，但是positive?報告一個錯誤，因為它的定義域僅是數字。為了使合約能取得我們對所有Racket值的意圖，我們可以確定這個數值既是一個數值同時也是正的，用and/c結合兩個合約：

(provide (contract-out [amount (and/c number? positive?)]))

7.1.2 合約與子產品的測試

在這一章中的所有合約和子產品（不包括那些隻是跟随的是使用描述子產品的标準#lang文法編寫。由于子產品充當一個合約中各方之間的邊界，是以示例涉及多個子產品。

為了在一個單一的子產品内或者在DrRacket的定義範圍（definitions area）内用多個子產品進行測試，使用Racket的子子產品。例如，嘗試如下所示本節中早先的示例：

#lang racket

(module+ server

(provide (contract-out [amount (and/c number? positive?)]))

(define amount 150))

(module+ main

(require (submod ".." server))

(+ amount 10))

每個子產品及其合約都用前面的module+關鍵字包裹在圓括号中。module後面的第一個表是該子產品的名稱，它被用在一個随後的require語句中（其中通過一個require每個引用用".."對名稱進行字首）。

7.1.3 嵌套合約邊界測試

在許多情況下，在子產品邊界上附加合約是有意義的。然而，能夠以一個比子產品更細緻的方式使用合約通常是友善的。這個define/contract表提供這種使用的權利：

#lang racket

(define/contract amount

(and/c number? positive?)

150)

(+ amount 10)

在這個例子中，define/contract表确定在amount的定義與其周邊上下文之間的一個合約邊界。換言之，這裡的雙方是這個定義及包含它的這個子產品。

創造這些嵌套合約邊界（nested contract boundaries）的表有時對使用來說是微妙的，因為它們也許有意想不到的性能影響或歸咎于似乎不直覺的一方。這些微妙之處在《使用define/contract和 ->》和《合約邊界和define/contract》中被講解。

7.2 函數的簡單合約

一個數學函數有一個定義域(domain)和一個值域(range)。定義域表示這個函數可以作為參數接受的值的類型，值域表示它生成的值的類型。用其定義域和值域描述一個函數的正常符号是

f : A -> B

這裡A是這個函數的定義域，B是值域。

一個程式設計語言中的函數也有定義域和值域，而一個合約可以確定一個函數在其定義域中隻接收值并且在其值域中隻産生值。一個->為一個函數建立這樣的一個合約。一個->之後的表為定義域指定定義域并且最後為值域指定一個合約。

這裡有一個可以代表一個銀行帳戶的子產品：

#lang racket

(provide (contract-out

[deposit (-> number? any)]

[balance (-> number?)]))

(define amount 0)

(define (deposit a) (set! amount (+ amount a)))

(define (balance) amount)

這個子產品輸出兩個函數：

• deposit，它接受一個數字并傳回某個未在合約中指定的值，
• balance，它傳回訓示賬戶目前餘額的一個數值。

當一個子產品輸出一個函數時，它在自己作為“伺服器（server）”與“用戶端（client）”的輸入這個函數的子產品之間建立兩個通信通道。如果用戶端子產品調用該函數，它發送一個值進入伺服器子產品。相反，如果這樣一個函數調用結束并且這個函數傳回一個值，這個伺服器子產品發送一個值回到用戶端子產品。這種用戶端-伺服器差別是很重要的，因為當出現問題時，一方或另一方将被歸咎。

如果一個用戶端子產品準備應用deposit到'millions，這将違反其合約。合約監視系統會獲得這個違規并因為與上述子產品違背合約而歸咎于這個用戶端。相比之下，如果balance函數準備傳回'broke，合同監視系統将歸咎于伺服器子產品。

一個->本身不是一個合約；它是一種合約組合（contract combinator），它結合其它合約以構成一個合約。

7.2.1 ->類型

如果你已經習慣了數學函數，你可以選擇一個合約箭頭出現在函數的定義域和值域之間而不是在開頭。如果你已經閱讀過《How to Design Programs》，那你已經見過這個很多次了。事實上，你也許已經在其他人的代碼中看到比如這些合約：

(provide (contract-out

[deposit (number? . -> . any)]))

如果一個Racket的S表達式包含在中間帶一個符号的兩個點，讀取器重新安排這個S表達式并放置符号到前面，就如《清單和Racket文法》裡描述的那樣。是以，

(number? . -> . any)

隻是編寫的另一種方式

(-> number? any)

7.2.2 使用define/contract和 ->

在《嵌套合約邊界測試》中引入的define/contract表也可以用來定義合約中的函數。例如,

(define/contract (deposit amount)

(-> number? any)

; 實作在這裡進行

....)

它用合約更早定義deposit函數。請注意，這對deposit的使用有兩個潛在的重要影響：

1. 由于合約總是在調用deposit時進行檢查，即使在定義它的子產品内，這也可能增加合約被檢查的次數。這可能導緻一個性能下降。如果函數在循環中反複調用或使用遞歸時尤其如此。
2. 在某些情況下，當在同一子產品中被其它代碼調用時，一個函數可以編寫來接受一組更寬松的輸入。對于此類用例，通過define/contract建立的合約邊界過于嚴格。

7.2.3 any和any/c

用于deposit的any合約比對任何結果，并且它隻能用于一個函數合約的值域位置。代替上面的any，我們可以使用更具體的合約void?，它表示函數總會傳回(void)值。然而，void?合約會要求合約監視系統每次在函數被調用時去檢查這個傳回值，即使“用戶端”子產品不能很好用這個值工作。相反，any告訴監視系統不檢查這個傳回值，它告訴一個潛在用戶端這個“伺服器”子產品對這個函數的傳回值不作任何承諾，甚至不管它是一個單獨的值或多個值。

any/c合約類似于any，在那裡它對一個值不做要求。不像any，any/c表示一個單個值，并且它适合用作一個參數合約。使用any/c作為一個值域合約強迫一個對這個函數産生一個單個值的檢查。就像這樣，

(-> integer? any)

描述一個接受一個整數并傳回任意數值的函數，然而

(-> integer? any/c)

描述接受一個整數并生成一個單個結果（但對結果沒有更多說明）的一個函數。以下函數

(define (f x) (values (+ x 1) (- x 1)))

比對(-> integer? any)，但不比對(-> integer? any/c)。

當對承諾來自一個函數的一個單個結果特别重要時，使用any/c作為一個結果合約。當你希望對一個函數的結果盡可能少地承諾（并盡可能少地檢查）時，使用any/c。

7.2.4 運轉你自己的合約

deposit函數将給定的數值添加到amount中。當該函數的合約阻止用戶端将它應用到非數值時，這個合約仍然允許它們把這個函數應用到複數、負數或不精确的數字中，但沒有一個能合理地表示錢的金額。

合約系統允許程式員定義他們自己的合約作為函數：

#lang racket

(define (amount? a)

(and (number? a) (integer? a) (exact? a) (>= a 0)))

(provide (contract-out

; 一個金額是一個美分的自然數

; 是給定的數字的一個amount?

[deposit (-> amount? any)]

[amount? (-> any/c boolean?)]

[balance (-> amount?)]))

(define amount 0)

(define (deposit a) (set! amount (+ amount a)))

(define (balance) amount)

這個子產品定義了一個amount?函數并在->合約内使用它作為一個合約。當一個用戶端用(-> amount? any)調用deposit函數作為輸出時，它必須提供一個精确的、非負的整數，否則amount?函數應用到參數将傳回#f，這将導緻合約監視系統歸咎于用戶端。類似地，伺服器子產品必須提供一個精确的、非負的整數作為balance的結果以保持無可歸咎。

當然，将一個通信通道限制為用戶端不明白的值是沒有意義的。是以，這個子產品也輸出amount?判斷本身，用一個合約表示它接受一個任意值并傳回一個布爾值。

在這種情況下，我們也可以使用natural-number/c代替amount?，因為它恰恰意味着相同的檢查：

(provide (contract-out

[deposit (-> natural-number/c any)]

[balance (-> natural-number/c)]))

接受一個參數的每一個函數可以當作一個判斷進而被用作一個合約。然而，為了結合現有的對一個新參數的檢查，合約連接配接符像and/c或or/c往往是有用的。例如，這裡還有另一種途徑去編寫上述合約：

(define amount/c

(and/c number? integer? exact? (or/c positive? zero?)))

(provide (contract-out

[deposit (-> amount/c any)]

[balance (-> amount/c)]))

其它值也作為合約提供雙重任務。例如，如果一個函數接受一個數值或#f，(or/cnumber? #f)就夠了。同樣，amount/c合約也許已經用一個0代替zero?來編寫。如果你使用一個正規表達式作為一個合約，該合約接受與正規表達式比對的字元串和位元組字元串。

當然，你可以用連接配接符像and/c混合你自己的合約執行函數。這裡有一個用于建立來自于銀行記錄的字元串的子產品：

#lang racket

(define (has-decimal? str)

(define L (string-length str))

(and (>= L 3)

(char=? #\. (string-ref str (- L 3)))))

(provide (contract-out

; 轉換一個随機數為一個字元串

[format-number (-> number? string?)]

; 用一個十進制點轉換一個金額為一個字元串，

; 就像在美國貨币的一個金額那樣。

[format-nat (-> natural-number/c

(and/c string? has-decimal?))]))

輸出函數format-number的合約指定該函數接受一個數值并生成一個字元串。這個輸出函數format-nat的合約比format-number的其中之一更有趣。它隻接受自然數。它的值域合約承諾在右邊的第三個位置帶有一個.的字元串。

如果我們希望加強format-nat的值域合約的承諾，以便它隻接受帶數字和一個點的字元串，我們可以這樣編寫：

#lang racket

(define (digit-char? x)

(member x '(#\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9 #\0)))

(define (has-decimal? str)

(define L (string-length str))

(and (>= L 3)

(char=? #\. (string-ref str (- L 3)))))

(define (is-decimal-string? str)

(define L (string-length str))

(and (has-decimal? str)

(andmap digit-char?

(string->list (substring str 0 (- L 3))))

(andmap digit-char?

(string->list (substring str (- L 2) L)))))

....

(provide (contract-out

....

; 轉換美分的一個金額（自然數）

; 成為一個基于美元的字元串

[format-nat (-> natural-number/c

(and/c string?

is-decimal-string?))]))

另外，在這種情況下，我們可以使用一個正規表達式作為一個合約：

#lang racket

(provide

(contract-out

....

; 轉換美分的一個數量（自然數）

; 成為一個基于美元的字元串

[format-nat (-> natural-number/c

(and/c string? #rx"[0-9]*\\.[0-9][0-9]"))]))

7.2.5 高階函數的合約

函數合約不僅僅局限于在其定義域或值域上的簡單判斷。還包括它們自己的函數合約，能夠被用作參數及一個函數結果。

例如：

(-> integer? (-> integer? integer?))

是描述一個柯裡函數的一個合約。它比對接受一個參數的函數并接着在傳回另一個接受一個前面的第二個參數，最後傳回一個整數。如果一個伺服器用這個合約輸出一個函數make-adder，并且如果make-adder傳回一個函數外還傳回一個值，那麼這個伺服器應被歸咎。如果make-adder确實傳回一個函數，但這個傳回函數被應用于一個整數外還有一個值，則用戶端應被歸咎。

同樣，合約

(-> (-> integer? integer?) integer?)

描述接受其它函數作為其輸入的函數。如果一個伺服器用這個合約輸出一個函數twice并且twice被應用給一個帶一個參數的函數外還給一個值，那麼用戶端應被歸咎。如果twice被應用給一個帶一個參數的函數并且twice對一個整數調用這個給定的函數外還對一個值，那麼伺服器應被歸咎。

7.2.6 帶”???“的合約資訊

你編寫了你的子產品。你添加了合約。你将它們放入接口以便用戶端程式員擁有來自接口的所有資訊。這是一門藝術：

> (module bank-server racket     (provide      (contract-out       [deposit (-> (λ (x)                      (and (number? x) (integer? x) (>= x 0)))                    any)]))     (define total 0)     (define (deposit a) (set! total (+ a total))))

幾個用戶端使用了你的子產品。其他人轉而使用了他們的子產品。突然他們中的一個看到了這個錯誤消息：

> (require 'bank-server)

> (deposit -10)

deposit: contract violation

expected: ???

given: -10

in: the 1st argument of

(-> ??? any)

contract from: bank-server

blaming: top-level

(assuming the contract is correct)

at: eval:2.0

???在那裡代表什麼？如果我們有這樣一個資料類型的名字，就像我們有字元串、數字等等，那不是很好嗎？

針對這種情況，Racket提供了扁平命名合約（flat named contract）。在這一術語中使用“合約”表明合約是第一類值。這個“扁平（flat）”意味着資料的集合是内建的資料原子類的一個子集；它們由一個接受所有Racket值并産生一個布爾值的判斷來描述。這個“命名（named）”部分表示我們想要做的事情，它将去命名這個合約以便錯誤消息變得明白易懂：

> (module improved-bank-server racket     (provide      (contract-out       [deposit (-> (flat-named-contract                     'amount                     (λ (x)                       (and (number? x) (integer? x) (>= x 0))))                    any)]))     (define total 0)     (define (deposit a) (set! total (+ a total))))

用這個小小的更改，這個錯誤消息就變得相當易讀：

> (require 'improved-bank-server)

> (deposit -10)

deposit: contract violation

expected: amount

given: -10

in: the 1st argument of

(-> amount any)

contract from: improved-bank-server

blaming: top-level

(assuming the contract is correct)

at: eval:5.0

7.2.7 解析一個合約錯誤資訊

一般來說，每個合約錯誤資訊由六部分組成：

• 一個用合約關聯的函數或方法的名稱。而且這個短語“合約違反”或“違反合約”取決于是否這個合約被用戶端或伺服器違反；例如在前面的示例中：

  deposit: contract violation

  ；
• 一個被違反的合約的準确方面的描述，

  expected: amount

  given: -10

  ；
• 這個完整的合約加上一個路徑顯示哪個方面被違反，

  in: the 1st argument of

  (-> amount any)

  ；
• 合約被放置的這個子產品（或者更廣泛地說，合同所規定的邊界），

  contract from: improved-bank-server

  ；
• 哪個應被歸咎，

  blaming: top-level

  (assuming the contract is correct)

  ；
• 以及這個合約出現的源程式位置。

  at: eval:5.0

  。

7.3 一般功能合約

->合約構造器為帶有一個固定數量參數的函數工作，并且這裡這個結果合約不依賴于這個輸入參數。為了支援其它類型的函數，Racket提供額外的合約構造器，尤其是 ->*和->i。

7.3.1 可選參數

請看一個字元串處理子產品的摘錄，該靈感來自于《Scheme cookbook》：

#lang racket

(provide

(contract-out

; 用（可選的）char填充給定的左右兩個str以使其左右居中

;

[string-pad-center (->* (string? natural-number/c)

(char?)

string?)]))

(define (string-pad-center str width [pad #\space])

(define field-width (min width (string-length str)))

(define rmargin (ceiling (/ (- width field-width) 2)))

(define lmargin (floor (/ (- width field-width) 2)))

(string-append (build-string lmargin (λ (x) pad))

str

(build-string rmargin (λ (x) pad))))

這個子產品輸出string-pad-center，一個函數，它在中心用給定字元串建立一個給定的width的一個字元串。這個預設的填充字元是#\space；如果這個用戶端子產品希望使用一個不同的字元，它可以用第三個參數——一個重寫預設值的char——調用string-pad-center。

這個函數定義使用可選參數，它對于這種功能是合适的。這裡有趣的一點是string-pad-center的合約的表達方式。

合約組合器->*，要求幾組合約：

• 第一個是對所有必需參數的合約的一個括号組。在這個例子中，我們看到兩個：string?和natural-number/c。
• 第二個是對所有可選參數的合約的一個括号組：char?。
• 最後一個是一個單一的合約：函數的結果。

請注意，如果預設值不滿足合約，則不會獲得此接口的合約錯誤。如果不能信任你自己去正确獲得初始值，則需要在邊界上傳遞初始值。

7.3.2 剩餘參數

max操作符至少接受一個實數，但它接受任意數量的附加參數。你可以使用一個剩餘參數（rest argument）編寫其它此類函數，例如在max-abs中：

參見《申明一個剩餘（rest）參數》以擷取剩餘參數的介紹。

(define (max-abs n . rst)

(foldr (lambda (n m) (max (abs n) m)) (abs n) rst))

通過一個合約描述這個函數需要一個對->*進一步的擴充：一個#:rest關鍵字在必需參數和可選參數之後指定在一個參數清單上的一個合約：

(provide

(contract-out

[max-abs (->* (real?) () #:rest (listof real?) real?)]))

正如對->*的通常情況，必需參數合約被封閉在第一對括号中，在這種情況下是一個單一的實數。空括号表示沒有可選參數（不包含剩餘參數）。剩餘參數合約跟着#:rest；因為所有的額外的參數必須是實數，剩餘參數的清單必須滿足合約(listof real?)。

7.3.3 關鍵字參數

其實->合約構造器也包含對關鍵字參數的支援。例如，考慮這個函數，它建立一個簡單的GUI并向使用者詢問一個yes-or-no的問題：

參見《聲明關鍵字（keyword）參數》以擷取關鍵字參數的介紹。

#lang racket/gui

(define (ask-yes-or-no-question question

#:default answer

#:title title

#:width w

#:height h)

(define d (new dialog% [label title] [width w] [height h]))

(define msg (new message% [label question] [parent d]))

(define (yes) (set! answer #t) (send d show #f))

(define (no) (set! answer #f) (send d show #f))

(define yes-b (new button%

[label "Yes"] [parent d]

[callback (λ (x y) (yes))]

[style (if answer '(border) '())]))

(define no-b (new button%

[label "No"] [parent d]

[callback (λ (x y) (no))]

[style (if answer '() '(border))]))

(send d show #t)

answer)

(provide (contract-out

[ask-yes-or-no-question

(-> string?

#:default boolean?

#:title string?

#:width exact-integer?

#:height exact-integer?

boolean?)]))

如果你真的想通過一個GUI問一個yes或no的問題，你應該使用message-box/custom。對此事而論，通常會比用較“yes”或“no”更确切的回答來提供按鈕更好。

ask-yes-or-no-question的合約使用->，同樣的方式lambda（或基于define的函數）允許一個關鍵字先于一個函數正式的參數，->允許一個關鍵字先于一個函數合約的參數合約。在這種情況下，這個合約表明ask-yes-or-no-question必須接收四個關鍵字參數，每一個關鍵字為：#:default、#:title、#:width和#:height。如同在一個函數定義中，在->中關鍵字的順序相對于其它的每個來說對函數的用戶端無關緊要；隻有參數合約的相對順序沒有關鍵字問題。

7.3.4 可選關鍵字參數

當然，ask-yes-or-no-question（從上一個問題中引來）中有許多參數有合理的預設值并且應該被設為可選的：

(define (ask-yes-or-no-question question

#:default answer

#:title [title "Yes or No?"]

#:width [w 400]

#:height [h 200])

...)

要指定這個函數的合約，我們需要再次使用->*。它支援關鍵字，正如你在可選參數和強制參數部分中所期望的一樣。在這種情況下，我們有強制關鍵字#:default和可選關鍵字#:title、#:width和#:height。是以，我們像這樣編寫合約：

(provide (contract-out

[ask-yes-or-no-question

(->* (string?

#:default boolean?)

(#:title string?

#:width exact-integer?

#:height exact-integer?)

boolean?)]))

也就是說，我們把強制關鍵字方在第一部分中，同時我們把可選關鍵字放在在第二部分中。

7.3.5 case-lambda的合約

用case-lambda定義的一個函數可以對其參數施加不同的限制取決于多少參數被提供。例如，report-cost函數可以既可以轉換一對數值也可以轉換一個字元串為一個新字元串：

參見《實參數量感覺函數：case-lambda》以獲得case-lambda的介紹。

(define report-cost   (case-lambda     [(lo hi) (format "between $~a and $~a" lo hi)]     [(desc) (format "~a of dollars" desc)]))

> (report-cost 5 8) "between $5 and $8" > (report-cost "millions") "millions of dollars"

對這樣的一個函數的合約用case->組合器構成，它根據需要組合多個功能合約：

(provide (contract-out

[report-cost

(case->

(integer? integer? . -> . string?)

(string? . -> . string?))]))

如你所見，report-cost的合約組合了兩個函數合約，它與其功能所需的解釋一樣多的從句。

7.3.6 參數和結果依賴

以下是來自一個虛構的數值子產品的一個摘錄：

(provide

(contract-out

[real-sqrt (->i ([argument (>=/c 1)])

[result (argument) (<=/c argument)])]))

這個詞“indy”意味着暗示歸咎會被配置設定到合約本身，因為這個合約必須被認為是一個獨立的元件。響應兩個現有标簽選擇名稱——“lax”和“picky”——為在研究文獻中的函數合約的不同語義。

這個輸出函數real-sqrt的合約使用->i比使用->*更好。這個“i”代表是一個印地依賴（indy dependent）合約，意味函數值域的合約依賴于該參數的值。在result的合約這一行裡argument的出現意味着那個結果依賴于這個參數。在特别情況下，real-sqrt的參數大于或等于1，是以一個很基本的正确性檢查是結果小于參數。

一般來說，一個依賴函數合約看起來更像一般的->*合約，但是在合約的其它地方可以使用名字。

回到銀行帳戶示例，假設我們一般化這個子產品以支援多個帳戶并且我們也包括一個取款操作。 改進後的銀行帳戶子產品包括一個account結構類型和以下函數：

(provide (contract-out

[balance (-> account? amount/c)]

[withdraw (-> account? amount/c account?)]

[deposit (-> account? amount/c account?)]))

但是，除了要求一個用戶端為一個取款提供一個有效金額外，金額應小于或等于指定賬戶的餘額，并且結果賬戶會比它開始時的錢少。同樣，該子產品可能承諾一個存款通過為賬戶增加錢來産生一個帳戶。以下實作通過合約強制執行這些限制和保證：

#lang racket

; 第1部分：合約定義

(struct account (balance))

(define amount/c natural-number/c)

; 第2部分：輸出

(provide

(contract-out

[create   (amount/c . -> . account?)]

[balance  (account? . -> . amount/c)]

[withdraw (->i ([acc account?]

[amt (acc) (and/c amount/c (<=/c (balance acc)))])

[result (acc amt)

(and/c account?

(lambda (res)

(>= (balance res)

(- (balance acc) amt))))])]

[deposit  (->i ([acc account?]

[amt amount/c])

[result (acc amt)

(and/c account?

(lambda (res)

(>= (balance res)

(+ (balance acc) amt))))])]))

; 第3部分：函數定義

(define balance account-balance)

(define (create amt) (account amt))

(define (withdraw a amt)

(account (- (account-balance a) amt)))

(define (deposit a amt)

(account (+ (account-balance a) amt)))

在第2部分中這個合約為create和balance提供了典型的類型保證。然而，對于withdraw和deposit，該合約檢查并保證對balance和deposit的更為複雜的限制。在對withdraw的合約上的第二個參數使用(balance acc)來檢查所提供的取款金額是否足夠小，其中acc是在->i之中給定的函數第一個參數的名稱。在withdraw結果上的合約使用acc和amt來保證不超過所要求的金額被提取。在deposit上的合約同樣在結果合約中使用acc和amount來保證至少和提供的一樣多的錢被存入賬戶。

正如上面所編寫的，當一個合約檢查失敗時，該錯誤消息不是很顯著。下面的修訂在一個助手函數mk-account-contract中使用flat-named-contract以提供更好的錯誤消息。

#lang racket

; 第1部分：合約定義

(struct account (balance))

(define amount/c natural-number/c)

(define msg> "account a with balance larger than ~a expected")

(define msg< "account a with balance less than ~a expected")

(define (mk-account-contract acc amt op msg)

(define balance0 (balance acc))

(define (ctr a)

(and (account? a) (op balance0 (balance a))))

(flat-named-contract (format msg balance0) ctr))

; 第2部分：導出

(provide

(contract-out

[create   (amount/c . -> . account?)]

[balance  (account? . -> . amount/c)]

[withdraw (->i ([acc account?]

[amt (acc) (and/c amount/c (<=/c (balance acc)))])

[result (acc amt) (mk-account-contract acc amt >= msg>)])]

[deposit  (->i ([acc account?]

[amt amount/c])

[result (acc amt)

(mk-account-contract acc amt <= msg<)])]))

; 第3部分：函數定義

(define balance account-balance)

(define (create amt) (account amt))

(define (withdraw a amt)

(account (- (account-balance a) amt)))

(define (deposit a amt)

(account (+ (account-balance a) amt)))

7.3.7 檢查狀态變化

->i合約組合器也可以確定一個函數僅按照一定的限制修改狀态。例如，考慮這個合約（它是來自架構中的函數preferences:add-panel的一個略微簡化的版本）：

(->i ([parent (is-a?/c area-container-window<%>)])

[_ (parent)

(let ([old-children (send parent get-children)])

(λ (child)

(andmap eq?

(append old-children (list child))

(send parent get-children))))])

它表示該函數接受一個被命名為parent的單一參數，并且parent必須是一個比對這個接口area-container-window<%>的對象。

這個值域合約確定該函數通過添加一個新的child到清單的前面來僅僅修改parent的children。它通過使用_代替一個正常的辨別符來完成這個，它告訴這個合約庫該值域合約并不依賴于任何結果的值，是以當這個函數被調用時，而不是傳回時，該合約庫求值這個跟着_的表達式。是以對get-children方法的調用發生在合約被調用下的函數之前。當合約下的函數傳回時，它的結果作為child被傳遞進去，并且合約確定該函數傳回後的child與該函數調用之前的child相同，但是有許許多多的child，在清單前面。

要去明白在一個集中在這點上的玩具例子中的不同，考慮這個程式：

#lang racket

(define x '())

(define (get-x) x)

(define (f) (set! x (cons 'f x)))

(provide

(contract-out

[f (->i () [_ (begin (set! x (cons 'ctc x)) any/c)])]

[get-x (-> (listof symbol?))]))

如果你将需要這個子產品，調用f，那麼get-x的結果會是'(f ctc)。相反，如果f的合約是

(->i () [res (begin (set! x (cons 'ctc x)) any/c)])

（隻改變res的下劃線），那麼get-x的結果會是'(ctc f)。

7.3.8 多個結果值

函數split接受char的一個清單并且傳遞在#\newline（如果有）的第一次出現之前的字元串以及這個清單的剩餘部分：

(define (split l)

(define (split l w)

(cond

[(null? l) (values (list->string (reverse w)) '())]

[(char=? #\newline (car l))

(values (list->string (reverse w)) (cdr l))]

[else (split (cdr l) (cons (car l) w))]))

(split l '()))

它是一個典型的多值函數，通過周遊一個單個清單傳回兩個值。

這樣一個函數的合約可以使用普通函數箭頭->，此後當它作為最後結果出現時，->特别地處理values：

(provide (contract-out

[split (-> (listof char?)

(values string? (listof char?)))]))

這樣一個函數的合約也可以使用->*編寫：

(provide (contract-out

[split (->* ((listof char?))

()

(values string? (listof char?)))]))

和前面一樣，帶->*的參數的合約被包裹在一對額外的圓括号中對（并且必須總是這樣被包裹）中，并且這個空括号對表示這裡沒有可選參數。這個結果的合約是在values内部：一個字元串和字元的一個清單。

現在，假設我們還希望確定split的第一個結果是在清單格式中的這個給定單詞的一個字首。在這種情況下，我們需要使用這個->i合約組合器：

(define (substring-of? s)

(flat-named-contract

(format "substring of ~s" s)

(lambda (s2)

(and (string? s2)

(<= (string-length s2) (string-length s))

(equal? (substring s 0 (string-length s2)) s2)))))

(provide

(contract-out

[split (->i ([fl (listof char?)])

(values [s (fl) (substring-of? (list->string fl))]

[c (listof char?)]))]))

像->*、->i組合使用函數中的參數來建立範圍的合約。是的，它不隻是傳回一個合約，而是函數産生值的數量：每個值的一個合約。在這種情況下，第二個合約和以前一樣，確定第二個結果是char清單。與此相反，第一個合約增強舊的，是以結果是給定單詞的字首。

當然，這個合約對于檢查來說是值得的。這裡有一個稍微廉價的版本：

(provide

(contract-out

[split (->i ([fl (listof char?)])

(values [s (fl) (string-len/c (length fl))]

[c (listof char?)]))]))

7.3.9 固定但靜态未知數量

想象一下你自己為一個函數編寫了一個合約，這個函數接受其它一些函數并且一個最終前者應用于後者的數值的清單。除非這個給定的函數的數量比對給定清單的長度，否則你的過程就會陷入困難。

考慮這個n-step函數：

; (number ... -> (union #f number?)) (listof number) -> void

(define (n-step proc inits)

(let ([inc (apply proc inits)])

(when inc

(n-step proc (map (λ (x) (+ x inc)) inits)))))

n-step的參數是proc，一個函數proc的結果要麼是數值要麼是假(false)，以及一個清單。它接着應用proc到這個清單inits中。隻要proc傳回一個數值，n-step把那個數值處理為一個在inits和遞歸裡的每個數值的增量值。當proc傳回false時，這個循環停止。

這裡有兩個應用：

; nat -> nat

(define (f x)

(printf "~s\n" x)

(if (= x 0) #f -1))

(n-step f '(2))

; nat nat -> nat

(define (g x y)

(define z (+ x y))

(printf "~s\n" (list x y z))

(if (= z 0) #f -1))

(n-step g '(1 1))

一個n-step的合約必須指定proc的行為的兩方面：其數量必須在inits裡包括元素的數量，同時它必須傳回一個數值或#f。後者是容易的，前者是困難的。乍一看，這似乎暗示一個合約配置設定了一個可變數量（variable-arity）給了proc：

(->* ()

#:rest (listof any/c)

(or/c number? false/c))

然而，這個合約表明這個函數必須接受任意（any）數量的參數，而不是一個特定（specific）的但不确定（undetermined）的數值。是以，應用n-step到(lambda (x) x)和(list 1)違反合約，因為這個給定的函數隻接受一個參數。

正确的合約使用unconstrained-domain->組合器，它僅指定一個函數的值域，而不是它的定義域。它接下來可能連接配接這個合約到一個數量測試以指定n-step的正确合約：

(provide

(contract-out

[n-step

(->i ([proc (inits)

(and/c (unconstrained-domain->

(or/c false/c number?))

(λ (f) (procedure-arity-includes?

f

(length inits))))]

[inits (listof number?)])

()

any)]))

7.4 合約：一個完整的例子

本節開發對于同一個例子的合約的幾種不同特點：Racket的argmax函數。根據它的Racket文檔，這個函數接受一個過程proc和一個非空的值清單，lst。它

傳回在最大化proc的結果的清單lst中的first元素。對first的強調是我們的。

例子：

> (argmax add1 (list 1 2 3))

3

> (argmax sqrt (list 0.4 0.9 0.16))

0.9

> (argmax second '((a 2) (b 3) (c 4) (d 1) (e 4)))

'(c 4)

這裡是這個函數的可能最簡單的合約：

version 1

#lang racket

(define (argmax f lov) ...)

(provide

(contract-out

[argmax (-> (-> any/c real?) (and/c pair? list?) any/c)]))

這個合約捕捉argmax的非正式描述的兩個必備條件：

• 這個給定的函數必須産生按<進行比較的數值。特别是，這個合約(-> any/c number?)不可行，因為number?也承認Racket中的複數有效。
• 給定清單必須至少包含一項。

當組合名稱時，合約解釋在同級的argmax的行為作為在一個子產品簽名（除空表方面外）中的一個ML（機器語言）函數類型。

然而，合約可能比一個類型簽名更值得關注。看一看argmax的第二個合約：

version 2

#lang racket

(define (argmax f lov) ...)

(provide

(contract-out

[argmax

(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()

(r (f lov)

(lambda (r)

(define [email protected] (f r))

(for/and ([v lov]) (>= [email protected] (f v))))))]))

它是一個依賴合約，它命名兩個參數并使用這個名稱在結果上添加一個判斷。這個判斷計算 (f r)——這裡r是argmax的結果——并接着驗證這個值大于或等于在lov的項目上的所有f值。

這是可能的嗎？——argmax會通過傳回一個随機值作弊，這個随機值意外地最大化f超過lov的所有元素。用一個合約，就有可能排除這種可能性：

version 2 rev. a

#lang racket

(define (argmax f lov) ...)

(provide

(contract-out

[argmax

(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()

(r (f lov)

(lambda (r)

(define [email protected] (f r))

(and (memq r lov)

(for/and ([v lov]) (>= [email protected] (f v)))))))]))

memq函數確定r是相等（intensionally equal）也就是說，那些喜歡在硬體層面思考的人的“指針相等（pointer equality）”。于lov的其中一個成員。當然，片刻的反思顯露出要構成這樣一個值是不可能的。函數是Racket中的不透明值，并且沒有應用一個函數，無法确定某個随機輸入值是否産生一個輸出值或觸發某些異常。是以我們從這裡開始忽略這種可能性。

版本2确切地闡述了argmax文檔的整體觀點，但它沒能傳達出這個結果是這個給定的最大化給定的函數f的清單的第一個元素。這是一個傳達這個非正式文檔的第二個方面的版本：

version 3

#lang racket

(define (argmax f lov) ...)

(provide

(contract-out

[argmax

(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()

(r (f lov)

(lambda (r)

(define [email protected] (f r))

(and (for/and ([v lov]) (>= [email protected] (f v)))

(eq? (first (memf (lambda (v) (= (f v) [email protected])) lov))

r)))))]))

那就是，memf函數确定lov的第一個元素，f下的lov的值等于f下的r的值。如果此元素是有意等于r，argmax的結果就是正确的。

第二個細化步驟介紹了兩個問題。首先，條件都重新計算lov的所有元素的f的值。第二，這個合約現在很難閱讀。合約應該有一個簡潔的表達方式，它可以讓一個用戶端可以用一個簡單的掃描進行了解。讓我們用具有合理意義的名稱的兩個輔助函來數消除可讀性問題：

version 3 rev. a

#lang racket

(define (argmax f lov) ...)

(provide

(contract-out

[argmax

(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()

(r (f lov)

(lambda (r)

(define [email protected] (f r))

(and (is-first-max? r [email protected] f lov)

(dominates-all [email protected] f lov)))))]))

; 這裡

;  [email protected]大于或等于在lov中v的所有(f v)

(define (dominates-all [email protected] f lov)

(for/and ([v lov]) (>= [email protected] (f v))))

;  r是eq?于lov的第一個元素v，因為它的(pred? v)

(define (is-first-max? r [email protected] f lov)

(eq? (first (memf (lambda (v) (= (f v) [email protected])) lov)) r))

原則上，這兩個判斷的名稱表示它們的功能和表達不需要讀取它們的定義。

這一步給我們帶來了新引進的低效率問題。為了避免因lov上的所有 v引起的(f v)的重複計算，我們改變合約以緻其計算這些值和重用它們是必要的：

version 3 rev. b

#lang racket

(define (argmax f lov) ...)

(provide

(contract-out

[argmax

(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()

(r (f lov)

(lambda (r)

(define [email protected] (f r))

(define flov (map f lov))

(and (is-first-max? r [email protected] (map list lov flov))

(dominates-all [email protected] flov)))))]))

; 這裡

;  [email protected]大于或等于flov中所有的[email protected]

(define (dominates-all [email protected] flov)

(for/and ([[email protected] flov]) (>= [email protected] [email protected])))

;  r是lov+flov裡第一個x的(first x)，整理為(= (second x) [email protected])

(define (is-first-max? r [email protected] lov+flov)

(define fst (first lov+flov))

(if (= (second fst) [email protected])

(eq? (first fst) r)

(is-first-max? r [email protected] (rest lov+flov))))

現在對結果的判斷為lov的元素再次計算了f的所有值一次。

單詞“eager（熱切，急切）”來自于合約語言學文獻。

當版本3去調用f時也許還太急切。然而無論lov包含有多少成員，Racket的argmax總是調用f，讓我們想象一下，為了說明目的，我們自己的實作首先檢查清單是否是單體。如果是這樣，第一個元素将是lov的唯一進制素，在這種情況下就不需要計算(f r)。Racket的argmax隐含論證它不僅承諾第一個值，它最大化f超過lov但同樣f産生一個結果的值。 事實上，由于f可能發散或增加一些例外輸入，argmax應該盡可能避免調用f。

下面的合約示範了如何調整高階依賴合約，以避免過度依賴：

version 4

#lang racket

(define (argmax f lov)

(if (empty? (rest lov))

(first lov)

...))

(provide

(contract-out

[argmax

(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()

(r (f lov)

(lambda (r)

(cond

[(empty? (rest lov)) (eq? (first lov) r)]

[else

(define [email protected] (f r))

(define flov (map f lov))

(and (is-first-max? r [email protected] (map list lov flov))

(dominates-all [email protected] flov))]))))]))

; where

;  [email protected]大于或等于flov中所有的[email protected]

(define (dominates-all [email protected] lov) ...)

;  r是lov+flov裡第一個x的(first x)，整理為(= (second x) [email protected])

(define (is-first-max? r [email protected] lov+flov) ...)

注意，這種考慮不适用于一階合同的世界。隻有一個高階（或惰性）語言迫使程式員去以如此精确度去表達合約。

發散或異常提升函數的問題應該讓讀者對帶副作用的函數的一般性問題保持警惕。如果這個給定的函數f有明顯的影響——表明它把它的調用記錄到了一個檔案——那麼argmax的用戶端将能夠觀察每次調用argmax的兩套日志。确切地講，如果值清單包含多個元素，這個日志将包含lov上的每一個值的兩個f調用。如果f對于計算來說太昂貴，則加倍調用承受一個高成本。

用過度熱切的合約來避免這種成本以及來标志問題，一個合約系統可以記錄已約定的函數參數的i/o并使用這些散清單的相關規範。這是PLT研究中的一個課題。敬請關注。

7.5 結構上的合約

子產品以兩種方式處理結構。首先它們輸出struct的定義，即某種創造結構的資格、存取它們的字段的資格、修改它們的資格以及差別這種結構于世界上所有其它值的資格。其次，有時一個子產品輸出一個特定的結構并希望它的字段包含某種值。本節講解如何使用合約保護結構的兩種使用。

7.5.1 確定一個特定值

如果你的子產品定義了一個變量做為一個結構，那麼你可以使用struct/c指定結構的形态：

#lang racket

(require lang/posn)

(define origin (make-posn 0 0))

(provide (contract-out

[origin (struct/c posn zero? zero?)]))

在這個例子中，該子產品輸入一個代表位置的庫，它輸出一個posn結構。posn中的一個建立并輸出所代表的網格原點，即(0,0)。

又見vector/c及類似的對（扁平）複合資料的合約組合器。

7.5.2 確定所有值

《How to Design Programs》這本書教授了posn應該隻包含在它們兩個字段裡的數值。用合約我們可以執行以下這種非正式資料定義：

#lang racket

(struct posn (x y))

(provide (contract-out

[struct posn ((x number?) (y number?))]

[p-okay posn?]

[p-sick posn?]))

(define p-okay (posn 10 20))

(define p-sick (posn 'a 'b))

這個子產品輸出整個結構定義：posn、posn?、posn-x、posn-y、set-posn-x!和set-posn-y!。每個函數執行或承諾一個posn結構的這兩個字段是數值——當這些值穿過子產品邊界傳遞時。是以，如果一個用戶端在10和'a上調用posn，這個合約系統就發出一個合約違反信号。

然而，posn子產品内的p-sick的建立，并沒有違反該合約。這個函數posn在内部使用，是以'a和'b不穿過子產品邊界。同樣，當p-sick穿過posn的邊界時，該合約承諾一個posn?并且别的什麼也沒有。特别是，這個檢查并沒有需要p-sick的字段是數值。

用子產品邊界的合約檢查的聯系意味着p-okay和p-sick從一個用戶端的角度看起來相似，直到用戶端選取了以下片斷：

#lang racket

(require lang/posn)

... (posn-x p-sick) ...

使用posn-x是這個用戶端能夠找到一個posn在x字段裡包含的内容的唯一途徑。posn-x的應用程式發送回p-sick進入posn子產品以及發送回這個結果值——這裡的'a——給用戶端，再跨越子產品邊界。在這一點上，這個合約系統發現一個承諾被違反了。具體來說，posn-x沒有傳回一個數值但卻傳回了一個符号，是以應該被歸咎。

這個具體的例子表明，對一個違反合約的解釋并不總是指明錯誤的來源。好消息是，這個錯誤被定位在posn子產品内。壞消息是，這種解釋是誤導性的。雖然posn-x産生了一個符号而不是一個數值是真的，它是從符号建立了posn的這個程式員的責任，亦即這個程式員添加了

(define p-sick (posn 'a 'b))

到這個子產品中。是以，當你在尋找基于違反合約的bug時，把這個例子記在心裡。

如果我們想修複p-sick的合約以便在sick被輸出時這個錯誤被捕獲，一個單一的改變就足夠了：

(provide

(contract-out

...

[p-sick (struct/c posn number? number?)]))

更确切地說，代替作為一個直白的posn?的輸出p-sick，我們使用一個struct/c合約來執行對其元件的限制。

7.5.3 檢查資料結構的特性

用struct/c編寫的合約立即檢查資料結構的字段，但是有時這能夠對一個程式的性能具有災難性的影響，這個程式本身并不檢查整個資料結構。

作為一個例子，考慮二叉搜尋樹搜尋算法。一個二叉搜尋樹就像一個二叉樹，除了這些數值被組織在樹中以便快速搜尋這個樹。特别是，對于樹中的每個内部節點，左邊子樹中的所有數值都小于節點中的數值，同時右子樹中的所有數值都大于節點中的數值。

我們可以實作一個搜尋函數in?，它利用二叉搜尋樹結構的優勢。

#lang racket

(struct node (val left right))

; 利用二叉搜尋樹不變量，

; 确定二叉搜尋樹“b”中是否存在“n”。

(define (in? n b)

(cond

[(null? b) #f]

[else (cond

[(= n (node-val b))

#t]

[(< n (node-val b))

(in? n (node-left b))]

[(> n (node-val b))

(in? n (node-right b))])]))

; 一個識别二叉搜尋樹的判斷。

(define (bst-between? b low high)

(or (null? b)

(and (<= low (node-val b) high)

(bst-between? (node-left b) low (node-val b))

(bst-between? (node-right b) (node-val b) high))))

(define (bst? b) (bst-between? b -inf.0 +inf.0))

(provide (struct-out node))

(provide (contract-out

[bst? (any/c . -> . boolean?)]

[in? (number? bst? . -> . boolean?)]))

在一個完整的二叉搜尋樹中，這意味着in?函數隻需探索一個對數節點。

對in?的合約保證其輸入是一個二叉搜尋樹。但仔細的思考表明，該合約違背了二叉搜尋樹算法的目的。特别是，考慮到in?函數裡内部的cond。這是in?函數擷取其速度的地方：它避免在每次遞歸調用時搜尋整個子樹。現在把它與bst-between?函數比較。在這種情況下它傳回#t，它周遊整個樹，意味in?的加速沒有實作。

為了解決這個問題，我們可以利用一種新的政策來檢查這個二叉搜尋樹合約。特别是，如果我們隻檢查了in?看着的節點上的合約，我們仍然可以保證這個樹至少部分形成良好，但是沒有改變複雜性。

要做到這一點，我們需要使用struct/dc來定義bst-between?。像struct/c一樣，struct/dc為一個結構定義一個合約。與struct/c不同，它允許字段被标記為惰性，這樣當比對選擇器被調用時，這些合約才被檢查。同樣，它不允許将可變字段被标記為惰性。

struct/dc表接受這個結構的每個字段的一個合約并傳回結構上的一個合約。更有趣的是，struct/dc允許我們編寫依賴合約，也就是說，合約中的某些合約取決于其它字段。我們可以用這個去定義二叉搜尋樹合約：

#lang racket

(struct node (val left right))

; 确定“n”是否在二進制搜尋樹“b”中

(define (in? n b) ... as before ...)

; bst-between : number number -> contract

; 建構了一個二叉搜尋樹合約

; whose values are between low and high

(define (bst-between/c low high)

(or/c null?

(struct/dc node [val (between/c low high)]

[left (val) #:lazy (bst-between/c low val)]

[right (val) #:lazy (bst-between/c val high)])))

(define bst/c (bst-between/c -inf.0 +inf.0))

(provide (struct-out node))

(provide (contract-out

[bst/c contract?]

[in? (number? bst/c . -> . boolean?)]))

一般來說，struct/dc的每個使用都必須命名字段并且接着為每個字段指定合約。在上面，val字段是一個接受low與high之間的值的合約。left和right字段依賴于val的值，被它們的第二個子表達式所表示。他們也用#:lazy關鍵字标記以表明它們隻有當合适的存取器被結構執行個體被調用時應該被檢查。它們的合約是通過遞歸調用bst-between/c函數來建構的。綜合起來，這個合約確定了在原始示例中被檢查的bst-between?函數的同樣的事情，但這裡這個檢查隻發生在in?探索這個樹時。

雖然這個合約提高了in?的性能，把它恢複到無合約版本的對數行為上，但它仍然施加相當大的恒定開銷。是以，這個合約庫也提供define-opt/c，它通過優化其主體來降低常數因子。它的形态和上面的define一樣。它希望它的主體是一個合約并且接着優化該合約。

(define-opt/c (bst-between/c low high)

(or/c null?

(struct/dc node [val (between/c low high)]

[left (val) #:lazy (bst-between/c low val)]

[right (val) #:lazy (bst-between/c val high)])))

7.6 用#:exists和#:∃抽象合約

合約系統提供可以保護抽象化的存在性合約，確定你的子產品的用戶端不能依賴于為你的資料結構所做的精确表示選擇。

如果你不能容易地鍵入Unicode字元，你可以鍵入#:exists來代替#:∃；在DrRacket裡，鍵入\exists後跟着alt-\或control-（取決于你的平台）會生成∃。

contract-out表允許你編寫

#:∃ name-of-a-new-contract

作為其從句之一。這個聲明引進這個變量name-of-a-new-contract，将它綁定到一個新的隐藏關于它保護的值的資訊的合約。

作為一個例子，考慮這（簡單的）一列資料結構的實作：

#lang racket

(define empty '())

(define (enq top queue) (append queue (list top)))

(define (next queue) (car queue))

(define (deq queue) (cdr queue))

(define (empty? queue) (null? queue))

(provide

(contract-out

[empty (listof integer?)]

[enq (-> integer? (listof integer?) (listof integer?))]

[next (-> (listof integer?) integer?)]

[deq (-> (listof integer?) (listof integer?))]

[empty? (-> (listof integer?) boolean?)]))

此代碼純粹按照清單實作一個隊列，這意味着資料結構的用戶端可以對資料結構直接使用car和cdr（也許偶然地），進而在描述裡的任何改變（例如，對于一個更有效表示，它支援攤銷的固定時間隊列和隊列操作）可能會破壞客戶機代碼。

為確定這個隊列描述是抽象的，我們可以在contract-out表達式裡使用#:∃，就像這樣：

(provide

(contract-out

#:∃ queue

[empty queue]

[enq (-> integer? queue queue)]

[next (-> queue integer?)]

[deq (-> queue queue)]

[empty? (-> queue boolean?)]))

現在，如果資料結構的用戶端嘗試使用car和cdr，它們會收到一個錯誤，而不是用隊列内部的東西來搞砸。

也參見《存在的合約和判斷》。

7.7 附加執行個體

本節說明Racket合約實施的目前狀态，用一系列來自于《Design by Contract, by Example》[Mitchell02]的例子。

米切爾（Mitchell）和麥金（McKim）的合約設計準則DbC源于1970年代風格的代數規範。DbC的總體目标是依據它的觀察指定一個代數的構造器。當我們換種方式表達米切爾和麥金的術語同時我們用最适合的途徑，我們保留他們的術語“類”（classes）和“對象”（objects）：

• 從指令中分離查詢。

  一個查詢（query）傳回一個結果但不會改變一個對象的可觀察性。一個指令（command）改變一個對象的可見性但不傳回結果。在應用程式實作中一個指令通常傳回同一個類的一個新對象。

• 從派生查詢中分離基本查詢。

  一個派生查詢（derived query）傳回一個根據基本查詢可計算的結果。

• 對于每個派生查詢，編寫一個根據基本查詢指定結果的崗位條件合約。
• 對于每個指令，編寫一個根據基本查詢指定對可觀測性更改的崗位條件合約。
• 對于每個查詢和指令，決定一個合适的前置條件合約。

以下各節對應于在米切爾和麥金的書中的一章（但不是所有的章都顯示在這裡）。我們建議你先閱讀合約（在第一子產品的末尾附近），然後是實作（在第一個子產品中），然後是測試子產品（在每一節的結尾）。

米切爾和麥金使用Eiffel語言作為底層程式設計語言同時采用一個傳統的指令式程式設計風格。我們的長期目标是翻譯他們的例子為有應用價值的Racket、面向結構的指令式Racket以及Racket的類系統。

注：模仿米切爾和McKim的參數性非正式概念（參數多态性），我們用一類合約。在幾個地方，一類合約的使用改進了米切爾和麥金的設計（參見接口中的注釋）。

7.7.1 一個客戶管理器組建

為了更好地跟蹤漏洞（bug），這第一個子產品包含一個獨立子產品裡的一些結構定義。

#lang racket

; data definitions

(define id? symbol?)

(define id-equal? eq?)

(define-struct basic-customer (id name address) #:mutable)

; interface

(provide

(contract-out

[id?                   (-> any/c boolean?)]

[id-equal?             (-> id? id? boolean?)]

[struct basic-customer ((id id?)

(name string?)

(address string?))]))

; end of interface

該子產品包含使用上述内容的程式。

#lang racket

(require "1.rkt") ; the module just above

; implementation

; [listof (list basic-customer? secret-info)]

(define all '())

(define (find c)

(define (has-c-as-key p)

(id-equal? (basic-customer-id (car p)) c))

(define x (filter has-c-as-key all))

(if (pair? x) (car x) x))

(define (active? c)

(pair? (find c)))

(define not-active? (compose not active? basic-customer-id))

(define count 0)

(define (get-count) count)

(define (add c)

(set! all (cons (list c 'secret) all))

(set! count (+ count 1)))

(define (name id)

(define bc-with-id (find id))

(basic-customer-name (car bc-with-id)))

(define (set-name id name)

(define bc-with-id (find id))

(set-basic-customer-name! (car bc-with-id) name))

(define c0 0)

; end of implementation

(provide

(contract-out

; how many customers are in the db?

[get-count (-> natural-number/c)]

; is the customer with this id active?

[active?   (-> id? boolean?)]

; what is the name of the customer with this id?

[name      (-> (and/c id? active?) string?)]

; change the name of the customer with this id

[set-name  (->i ([id id?] [nn string?])

[result any/c] ; result contract

#:post (id nn) (string=? (name id) nn))]

[add       (->i ([bc (and/c basic-customer? not-active?)])

; A pre-post condition contract must use

; a side-effect to express this contract

; via post-conditions

#:pre () (set! c0 count)

[result any/c] ; result contract

#:post () (> count c0))]))

測試：

#lang racket

(require rackunit rackunit/text-ui "1.rkt" "1b.rkt")

(add (make-basic-customer 'mf "matthias" "brookstone"))

(add (make-basic-customer 'rf "robby" "beverly hills park"))

(add (make-basic-customer 'fl "matthew" "pepper clouds town"))

(add (make-basic-customer 'sk "shriram" "i city"))

(run-tests

(test-suite

"manager"

(test-equal? "id lookup" "matthias" (name 'mf))

(test-equal? "count" 4 (get-count))

(test-true "active?" (active? 'mf))

(test-false "active? 2" (active? 'kk))

(test-true "set name" (void? (set-name 'mf "matt")))))

7.7.2 一個參數化（簡單）棧

#lang racket

; a contract utility

(define (eq/c x) (lambda (y) (eq? x y)))

(define-struct stack (list p? eq))

(define (initialize p? eq) (make-stack '() p? eq))

(define (push s x)

(make-stack (cons x (stack-list s)) (stack-p? s) (stack-eq s)))

(define (item-at s i) (list-ref (reverse (stack-list s)) (- i 1)))

(define (count s) (length  (stack-list s)))

(define (is-empty? s) (null? (stack-list s)))

(define not-empty? (compose not is-empty?))

(define (pop s) (make-stack (cdr (stack-list s))

(stack-p? s)

(stack-eq s)))

(define (top s) (car (stack-list s)))

(provide

(contract-out

; predicate

[stack?     (-> any/c boolean?)]

; primitive queries

; how many items are on the stack?

[count      (-> stack? natural-number/c)]

; which item is at the given position?

[item-at

(->d ([s stack?] [i (and/c positive? (<=/c (count s)))])

()

[result (stack-p? s)])]

; derived queries

; is the stack empty?

[is-empty?

(->d ([s stack?])

()

[result (eq/c (= (count s) 0))])]

; which item is at the top of the stack

[top

(->d ([s (and/c stack? not-empty?)])

()

[t (stack-p? s)] ; a stack item, t is its name

#:post-cond

([stack-eq s] t (item-at s (count s))))]

; creation

[initialize

(->d ([p contract?] [s (p p . -> . boolean?)])

()

; Mitchell and McKim use (= (count s) 0) here to express

; the post-condition in terms of a primitive query

[result (and/c stack? is-empty?)])]

; commands

; add an item to the top of the stack

[push

(->d ([s stack?] [x (stack-p? s)])

()

[sn stack?] ; result kind

#:post-cond

(and (= (+ (count s) 1) (count sn))

([stack-eq s] x (top sn))))]

; remove the item at the top of the stack

[pop

(->d ([s (and/c stack? not-empty?)])

()

[sn stack?] ; result kind

#:post-cond

(= (- (count s) 1) (count sn)))]))

測試：

#lang racket

(require rackunit rackunit/text-ui "2.rkt")

(define s0 (initialize (flat-contract integer?) =))

(define s2 (push (push s0 2) 1))

(run-tests

(test-suite

"stack"

(test-true

"empty"

(is-empty? (initialize (flat-contract integer?) =)))

(test-true "push" (stack? s2))

(test-true

"push exn"

(with-handlers ([exn:fail:contract? (lambda _ #t)])

(push (initialize (flat-contract integer?)) 'a)

#f))

(test-true "pop" (stack? (pop s2)))

(test-equal? "top" (top s2) 1)

(test-equal? "toppop" (top (pop s2)) 2)))

7.7.3 一個字典

#lang racket

; a shorthand for use below

(define-syntax ⇒

(syntax-rules ()

[(⇒ antecedent consequent) (if antecedent consequent #t)]))

; implementation

(define-struct dictionary (l value? eq?))

; the keys should probably be another parameter (exercise)

(define (initialize p eq) (make-dictionary '() p eq))

(define (put d k v)

(make-dictionary (cons (cons k v) (dictionary-l d))

(dictionary-value? d)

(dictionary-eq? d)))

(define (rem d k)

(make-dictionary

(let loop ([l (dictionary-l d)])

(cond

[(null? l) l]

[(eq? (caar l) k) (loop (cdr l))]

[else (cons (car l) (loop (cdr l)))]))

(dictionary-value? d)

(dictionary-eq? d)))

(define (count d) (length (dictionary-l d)))

(define (value-for d k) (cdr (assq k (dictionary-l d))))

(define (has? d k) (pair? (assq k (dictionary-l d))))

(define (not-has? d) (lambda (k) (not (has? d k))))

; end of implementation

; interface

(provide

(contract-out

; predicates

[dictionary? (-> any/c boolean?)]

; basic queries

; how many items are in the dictionary?

[count       (-> dictionary? natural-number/c)]

; does the dictionary define key k?

[has?        (->d ([d dictionary?] [k symbol?])

()

[result boolean?]

#:post-cond

((zero? (count d)) . ⇒ . (not result)))]

; what is the value of key k in this dictionary?

[value-for   (->d ([d dictionary?]

[k (and/c symbol? (lambda (k) (has? d k)))])

()

[result (dictionary-value? d)])]

; initialization

; post condition: for all k in symbol, (has? d k) is false.

[initialize  (->d ([p contract?] [eq (p p . -> . boolean?)])

()

[result (and/c dictionary? (compose zero? count))])]

; commands

; Mitchell and McKim say that put shouldn't consume Void (null ptr)

; for v. We allow the client to specify a contract for all values

; via initialize. We could do the same via a key? parameter

; (exercise). add key k with value v to this dictionary

[put         (->d ([d dictionary?]

[k (and/c symbol? (not-has? d))]

[v (dictionary-value? d)])

()

[result dictionary?]

#:post-cond

(and (has? result k)

(= (count d) (- (count result) 1))

([dictionary-eq? d] (value-for result k) v)))]

; remove key k from this dictionary

[rem         (->d ([d dictionary?]

[k (and/c symbol? (lambda (k) (has? d k)))])

()

[result (and/c dictionary? not-has?)]

#:post-cond

(= (count d) (+ (count result) 1)))]))

; end of interface

測試：

#lang racket

(require rackunit rackunit/text-ui "3.rkt")

(define d0 (initialize (flat-contract integer?) =))

(define d (put (put (put d0 'a 2) 'b 2) 'c 1))

(run-tests

(test-suite

"dictionaries"

(test-equal? "value for" 2 (value-for d 'b))

(test-false "has?" (has? (rem d 'b) 'b))

(test-equal? "count" 3 (count d))

(test-case "contract check for put: symbol?"

(define d0 (initialize (flat-contract integer?) =))

(check-exn exn:fail:contract? (lambda () (put d0 "a" 2))))))

7.7.4 一個隊列

#lang racket

; Note: this queue doesn't implement the capacity restriction

; of Mitchell and McKim's queue but this is easy to add.

; a contract utility

(define (all-but-last l) (reverse (cdr (reverse l))))

(define (eq/c x) (lambda (y) (eq? x y)))

; implementation

(define-struct queue (list p? eq))

(define (initialize p? eq) (make-queue '() p? eq))

(define items queue-list)

(define (put q x)

(make-queue (append (queue-list q) (list x))

(queue-p? q)

(queue-eq q)))

(define (count s) (length  (queue-list s)))

(define (is-empty? s) (null? (queue-list s)))

(define not-empty? (compose not is-empty?))

(define (rem s)

(make-queue (cdr (queue-list s))

(queue-p? s)

(queue-eq s)))

(define (head s) (car (queue-list s)))

; interface

(provide

(contract-out

; predicate

[queue?     (-> any/c boolean?)]

; primitive queries

; Imagine providing this 'query' for the interface of the module

; only. Then in Racket there is no reason to have count or is-empty?

; around (other than providing it to clients). After all items is

; exactly as cheap as count.

[items      (->d ([q queue?]) () [result (listof (queue-p? q))])]

; derived queries

[count      (->d ([q queue?])

; We could express this second part of the post

; condition even if count were a module "attribute"

; in the language of Eiffel; indeed it would use the

; exact same syntax (minus the arrow and domain).

()

[result (and/c natural-number/c

(=/c (length (items q))))])]

[is-empty?  (->d ([q queue?])

()

[result (and/c boolean?

(eq/c (null? (items q))))])]

[head       (->d ([q (and/c queue? (compose not is-empty?))])

()

[result (and/c (queue-p? q)

(eq/c (car (items q))))])]

; creation

[initialize (-> contract?

(contract? contract? . -> . boolean?)

(and/c queue? (compose null? items)))]

; commands

[put        (->d ([oldq queue?] [i (queue-p? oldq)])

()

[result

(and/c

queue?

(lambda (q)

(define old-items (items oldq))

(equal? (items q) (append old-items (list i)))))])]

[rem        (->d ([oldq (and/c queue? (compose not is-empty?))])

()

[result

(and/c queue?

(lambda (q)

(equal? (cdr (items oldq)) (items q))))])]))

; end of interface

測試：

#lang racket

(require rackunit rackunit/text-ui "5.rkt")

(define s (put (put (initialize (flat-contract integer?) =) 2) 1))

(run-tests

(test-suite

"queue"

(test-true

"empty"

(is-empty? (initialize (flat-contract integer?) =)))

(test-true "put" (queue? s))

(test-equal? "count" 2 (count s))

(test-true "put exn"

(with-handlers ([exn:fail:contract? (lambda _ #t)])

(put (initialize (flat-contract integer?)) 'a)

#f))

(test-true "remove" (queue? (rem s)))

(test-equal? "head" 2 (head s))))

7.8 建立新合約

合約在内部作為函數來表示，這個函數接受關于合約的資訊（歸咎于誰、源程式位置等等）并産生執行合約的推斷（本着Dana Scott的精神）。

一般意義上，一個推斷是接受一個任意值的一個函數，并傳回滿足相應合約的一個值。例如，隻接受整數的一個推斷對應于合約(flat-contract integer?)，同時可以這樣編寫：

(define int-proj

(λ (x)

(if (integer? x)

x

(signal-contract-violation))))

作為第二個例子，接受整數上的一進制函數的一個推斷看起來像這樣：

(define int->int-proj

(λ (f)

(if (and (procedure? f)

(procedure-arity-includes? f 1))

(λ (x) (int-proj (f (int-proj x))))

(signal-contract-violation))))

雖然這些推斷具有恰當的錯誤行為，但它們還不太适合作為合約使用，因為它們不容納歸咎也不提供良好的錯誤消息。為了适應這些，合約不隻使用簡單的推斷，而是使用接受一個歸咎對象（blame object）的函數将被歸咎雙方的名字封裝起來，以及合約建立的源代碼位置和合約名稱的記錄。然後，它們可以依次傳遞這些資訊給raise-blame-error來發出一個良好的錯誤資訊。

這裡是這兩個推斷中的第一個，被重寫以在合約系統中使用：

(define (int-proj blame)

(λ (x)

(if (integer? x)

x

(raise-blame-error

blame

x

'(expected: "<integer>" given: "~e")

x))))

新的論據指明了誰将因為正數和負數的合約違約被歸咎。

在這個系統中，合約總是建立在雙方之間。一方稱為伺服器，根據這個合約提供一些值；另一方稱為用戶端，也根據這個合約接受這些值。伺服器稱為主動位置，用戶端稱為被動位置。是以，對于僅在整數合約的情況下，唯一可能出錯的是所提供的值不是一個整數。是以，永遠隻有主動的一方（伺服器）才能獲得歸咎。raise-blame-error函數總是歸咎主動的一方。

與我們的函數合約的推斷的比較：

(define (int->int-proj blame)

(define dom (int-proj (blame-swap blame)))

(define rng (int-proj blame))

(λ (f)

(if (and (procedure? f)

(procedure-arity-includes? f 1))

(λ (x) (rng (f (dom x))))

(raise-blame-error

blame

f

'(expected "a procedure of one argument" given: "~e")

f))))

在這種情況下，唯一明确的歸咎涵蓋了一個提供給合約的非過程或一個這個不接受一個參數的過程的情況。與整數推斷一樣，這裡的歸咎也在于這個值的生成器，這就是為什麼raise-blame-error傳遞沒有改變的blame。

對于定義域和值域的檢查被委托給了int-proj函數，它在int->int-proj函數的前面兩行提供其參數。這裡的訣竅是，即使int->int-proj函數總是歸咎于它所認為的主動方，我們可以通過在給定的歸咎對象（blame object）上調用blame-swap來互換歸咎方，用被動方更換主動方，反之亦然。

然而，這種技術并不僅僅是一個讓這個例子工作的廉價技巧。主動方和被動方的反轉是一個函數行為方式的自然結果。也就是說，想象在兩個子產品之間的一個程式裡的值流。首先，一個子產品（伺服器）定義了一個函數，然後那個子產品被另一個子產品（用戶端）所依賴。到目前為止，這個函數本身必須從原始出發，提供子產品給這個需求子產品。現在，假設需求子產品調用這個函數，為它提供一個參數。此時，值流逆轉。這個參數正在從需求子產品回流到提供的子產品！這個用戶端正在“提供”參數給伺服器，并且這個伺服器正在作為用戶端接收那個值。最後，當這個函數産生一個結果時，那個結果在原始方向上從伺服器回流到用戶端。是以，定義域上的合約倒轉了主動的和被動的歸咎方，就像值流逆轉一樣。

我們可以利用這個領悟來概括函數合約并建構一個函數，它接受任意兩個合約并為它們之間的函數傳回一個合約。

這一推斷也走的更遠而且在一個合約違反被檢測到時使用blame-add-context來改進錯誤資訊。

(define (make-simple-function-contract dom-proj range-proj)

(λ (blame)

(define dom (dom-proj (blame-add-context blame

"the argument of"

#:swap? #t)))

(define rng (range-proj (blame-add-context blame

"the range of")))

(λ (f)

(if (and (procedure? f)

(procedure-arity-includes? f 1))

(λ (x) (rng (f (dom x))))

(raise-blame-error

blame

f

'(expected "a procedure of one argument" given: "~e")

f)))))

雖然這些推斷得到了合約庫的支援并且可以用來建構新合約，但是這個合約庫也為了更有效的推斷支援一個不同的API。具體來說，一個後負推斷（late neg projection）接受一個不帶反面歸咎的資訊的歸咎對象，然後按照這個順序傳回一個函數，它既接受合約約定的值也接受該被動方的名稱。這個傳回函數接着依次根據合約傳回值。看起來像這樣重寫int->int-proj以使用這個API：

(define (int->int-proj blame)   (define dom-blame (blame-add-context blame                                        "the argument of"                                        #:swap? #t))   (define rng-blame (blame-add-context blame "the range of"))   (define (check-int v to-blame neg-party)     (unless (integer? v)       (raise-blame-error        to-blame #:missing-party neg-party        v        '(expected "an integer" given: "~e")        v)))   (λ (f neg-party)     (if (and (procedure? f)              (procedure-arity-includes? f 1))         (λ (x)           (check-int x dom-blame neg-party)           (define ans (f x))           (check-int ans rng-blame neg-party)           ans)         (raise-blame-error          blame #:missing-party neg-party          f          '(expected "a procedure of one argument" given: "~e")          f))))

這種類型的合約的優點是，blame參數能夠在合同邊界的伺服器一邊被提供，而且這個結果可以被用于每個不同的用戶端。在較簡單的情況下，一個新的歸咎對象必須為每個用戶端被建立。

最後一個問題在這個合約能夠與剩餘的合約系統一起使用之前任然存在。在上面的函數中，這個合約通過為f建立一個包裝函數來實作，但是這個包裝器函數與equal?不協作，它也不讓運作時系統知道這裡有一個結果函數與輸入函數f之間的聯系。

為了解決這兩個問題，我們應該使用監護（chaperones）而不是僅僅使用λ來建立包裝器函數。這裡是這個被重寫以使用監護的int->int-proj函數：

(define (int->int-proj blame)   (define dom-blame (blame-add-context blame                                        "the argument of"                                        #:swap? #t))   (define rng-blame (blame-add-context blame "the range of"))   (define (check-int v to-blame neg-party)     (unless (integer? v)       (raise-blame-error        to-blame #:missing-party neg-party        v        '(expected "an integer" given: "~e")        v)))   (λ (f neg-party)     (if (and (procedure? f)              (procedure-arity-includes? f 1))         (chaperone-procedure          f          (λ (x)            (check-int x dom-blame neg-party)            (values (λ (ans)                      (check-int ans rng-blame neg-party)                      ans)                    x)))         (raise-blame-error          blame #:missing-party neg-party          f          '(expected "a procedure of one argument" given: "~e")          f))))

如上所述的推斷，但适合于其它，你可能制造的新類型的值，可以與合約庫原語一起使用。具體來說，我們能夠使用make-chaperone-contract來建構它：

(define int->int-contract   (make-contract    #:name 'int->int    #:late-neg-projection int->int-proj))

并且接着将其與一個值相結合并得到一些合約檢查。

(define/contract (f x)   int->int-contract   "not an int")

> (f #f) f: contract violation;  expected an integer   given: #f   in: the argument of       int->int   contract from: (function f)   blaming: top-level    (assuming the contract is correct)   at: eval:5.0 > (f 1) f: broke its own contract;  promised an integer   produced: "not an int"   in: the range of       int->int   contract from: (function f)   blaming: (function f)    (assuming the contract is correct)   at: eval:5.0

7.8.1 合約結構屬性

對于一次性合約來說make-chaperone-contract函數是可以的，但通常你想制定許多不同的合約，僅在某些方面不同。做到這一點的最好方法是使用一個struct，帶有prop:contract、prop:chaperone-contract或prop:flat-contract。

例如，假設我們想制定接受一個值域合約和一個定義域合約的->合約的一個簡單表。我們應該定義一個帶有兩個字段的結構并使用build-chaperone-contract-property來建構我們需要的監護合約屬性。

(struct simple-arrow (dom rng)   #:property prop:chaperone-contract   (build-chaperone-contract-property    #:name    (λ (arr) (simple-arrow-name arr))    #:late-neg-projection    (λ (arr) (simple-arrow-late-neg-proj arr))))

要像integer?和#f那樣對值進行自動強制，我們需要調用coerce-chaperone-contract（注意這個拒絕模拟合約并對扁平合約不予堅持；要去做那些事情中的任何一件，而不是調用coerce-contract或coerce-flat-contract）。

(define (simple-arrow-contract dom rng)   (simple-arrow (coerce-contract 'simple-arrow-contract dom)                 (coerce-contract 'simple-arrow-contract rng)))

去定義simple-arrow-name是直截了當的；它需要傳回一個表示合約的S表達式：

(define (simple-arrow-name arr)   `(-> ,(contract-name (simple-arrow-dom arr))        ,(contract-name (simple-arrow-rng arr))))

并且我們能夠使用我們前面定義的一個廣義的推斷來定義這個推斷，這次使用監護：

(define (simple-arrow-late-neg-proj arr)   (define dom-ctc (get/build-late-neg-projection (simple-arrow-dom arr)))   (define rng-ctc (get/build-late-neg-projection (simple-arrow-rng arr)))   (λ (blame)     (define dom+blame (dom-ctc (blame-add-context blame                                                   "the argument of"                                                   #:swap? #t)))     (define rng+blame (rng-ctc (blame-add-context blame "the range of")))     (λ (f neg-party)       (if (and (procedure? f)                (procedure-arity-includes? f 1))           (chaperone-procedure            f            (λ (arg)              (values               (λ (result) (rng+blame result neg-party))               (dom+blame arg neg-party))))           (raise-blame-error            blame #:missing-party neg-party            f            '(expected "a procedure of one argument" given: "~e")            f)))))

(define/contract (f x)   (simple-arrow-contract integer? boolean?)   "not a boolean")

> (f #f) f: contract violation   expected: integer?   given: #f   in: the argument of       (-> integer? boolean?)   contract from: (function f)   blaming: top-level    (assuming the contract is correct)   at: eval:12.0 > (f 1) f: broke its own contract   promised: boolean?   produced: "not a boolean"   in: the range of       (-> integer? boolean?)   contract from: (function f)   blaming: (function f)    (assuming the contract is correct)   at: eval:12.0

7.8.2 使所有警告和報警一緻

這裡有一些對一個simple-arrow-contract沒有添加的合約的可選部分。在這一節中，我們通過所有的例子來展示它們是如何實作的。

首先是一個一階檢查。這是被or/c使用來确定那一個高階參數合約在它看到一個值時去使用。下面是我們簡單箭頭合約的函數。

(define (simple-arrow-first-order ctc)   (λ (v) (and (procedure? v)               (procedure-arity-includes? v 1))))

如果這個值确實不滿足合約，它接受一個值并傳回#f，并且如傳回#t，隻要我們能夠辨識，這個值滿足合約，隻是檢查值的一階屬性。

其次是随機生成。合約庫中的随機生成分為兩部分：随機生成滿足合約的值的能力以及運用比對這個給定合約的值的能力，希望發現其中的錯誤（并也試圖使它們産生令人感興趣的值以在生成期間被用于其它地方）。

為了運用合約，我們需要實作一個被給定一個arrow-contract結構的函數和一些輔助函數。它應該傳回兩個值：一個接受合約值并運用它們的函數；外加運用程序總會産生的一個值清單。在我們簡單合約的情況，我們知道我們總能産生值域的值，隻要我們能夠生成定義域的值（因為我們能夠僅調用這個函數）。是以，這裡有一個比對build-chaperone-contract-property的合約的exercise參數的函數：

(define (simple-arrow-contract-exercise arr)   (define env (contract-random-generate-get-current-environment))   (λ (fuel)     (define dom-generate       (contract-random-generate/choose (simple-arrow-dom arr) fuel))     (cond       [dom-generate        (values         (λ (f) (contract-random-generate-stash                 env                 (simple-arrow-rng arr)                 (f (dom-generate))))         (list (simple-arrow-rng arr)))]       [else        (values void '())])))

如果定義域合約可以被生成，那麼我們知道我們能夠通過運用做一些好的事情。在這種情況下，我們傳回一個過程，它用我們從定義域生成的東西調用f（比對這個合約函數），并且我們也在環境中隐藏這個結果值。我們也傳回(simple-arrow-rng arr)來表明運用總會産生那個合約的某些東西。

如果我們不能做到，那麼我們隻簡單地傳回一個函數，它不運用(void)和空清單（表示我們不會生成任何值）。

然後，為了生成與這個合約相比對的值，我們定義一個在給定合約和某些輔助函數時成為一個随機函數的函數。為了幫助它成為一個更有效的測試函數，我們可以運用它接受的任何參數，同時也将它們儲存到生成環境中，但前提是我們可以生成值域合約的值。

(define (simple-arrow-contract-generate arr)   (λ (fuel)     (define env (contract-random-generate-get-current-environment))     (define rng-generate       (contract-random-generate/choose (simple-arrow-rng arr) fuel))     (cond       [rng-generate        (λ ()          (λ (arg)            (contract-random-generate-stash env (simple-arrow-dom arr) arg)            (rng-generate)))]       [else        #f])))

當這個随機生成将某個東西拉出環境時，它需要能夠判斷一個被傳遞給contract-random-generate-stash的值是否是一個試圖生成的合約的候選對象。當然，合約傳遞給contract-random-generate-stash的是一個精确的比對，那麼它就能夠使用它。但是，如果這個合約更強（意思是它接受更少的值），它也能夠使用這個價值。

為了提供這個功能，我們實作這個函數：

(define (simple-arrow-first-stronger? this that)   (and (simple-arrow? that)        (contract-stronger? (simple-arrow-dom that)                            (simple-arrow-dom this))        (contract-stronger? (simple-arrow-rng this)                            (simple-arrow-rng that))))

這個函數接受this和that，兩個合約。它保證this将是我們的簡單箭頭合約之一，因為我們正在用簡單箭頭合約實作供應這個函數。但這個that參數也許是任何合約。如果同樣比較定義域和值域，這個函數檢查以弄明白是否that也是一個簡單箭頭合約。當然，那裡還有其它的合約，我們也可以檢查（例如，使用->或->*的合約建構），但我們并不需要。如果這個更強的函數不知道答案但如果它傳回#t，它被允許傳回#f，那麼這個合約必須真正變得更強。

既然我們有實作了的所有部分，我們需要傳遞它們給build-chaperone-contract-property，這樣合約系統就開始使用它們了：

(struct simple-arrow (dom rng)   #:property prop:custom-write contract-custom-write-property-proc   #:property prop:chaperone-contract   (build-chaperone-contract-property    #:name    (λ (arr) (simple-arrow-name arr))    #:late-neg-projection    (λ (arr) (simple-arrow-late-neg-proj arr))    #:first-order simple-arrow-first-order    #:stronger simple-arrow-first-stronger?    #:generate simple-arrow-contract-generate    #:exercise simple-arrow-contract-exercise))

(define (simple-arrow-contract dom rng)   (simple-arrow (coerce-contract 'simple-arrow-contract dom)                 (coerce-contract 'simple-arrow-contract rng)))

我們還添加了一個prop:custom-write屬性以便這個合約正确列印，例如：

> (simple-arrow-contract integer? integer?)

(-> integer? integer?)

（因為合約庫不能依賴于

#lang racket/generic

但仍然希望提供一些幫助以便于使用正确的列印機，我們使用prop:custom-write。）

既然那些已經完成，我們就能夠使用新功能。這裡有一個随機函數，它由合約庫生成，使用我們的simple-arrow-contract-generate函數：

(define a-random-function   (contract-random-generate    (simple-arrow-contract integer? integer?)))

> (a-random-function 0) > (a-random-function 1) -1730424298

這裡是是合約系統怎麼能在使用簡單箭頭合約的函數中立刻自動發現缺陷（bug）：

(define/contract (misbehaved-f f)   (-> (simple-arrow-contract integer? boolean?) any)   (f "not an integer"))

> (contract-exercise misbehaved-f) misbehaved-f: broke its own contract   promised: integer?   produced: "not an integer"   in: the argument of       the 1st argument of       (-> (-> integer? boolean?) any)   contract from: (function misbehaved-f)   blaming: (function misbehaved-f)    (assuming the contract is correct)   at: eval:25.0

并且如果我們沒有實作simple-arrow-first-order，那麼or/c就不能夠辨識這個程式中使用哪一個or/c分支：

(define/contract (maybe-accepts-a-function f)   (or/c (simple-arrow-contract real? real?)         (-> real? real? real?)         real?)   (if (procedure? f)       (if (procedure-arity-includes f 1)           (f 1132)           (f 11 2))       f))

> (maybe-accepts-a-function sqrt) maybe-accepts-a-function: contract violation   expected: real?   given: #<procedure:sqrt>   in: the argument of       a part of the or/c of       (or/c        (-> real? real?)        (-> real? real? real?)        real?)   contract from:       (function maybe-accepts-a-function)   blaming: top-level    (assuming the contract is correct)   at: eval:27.0 > (maybe-accepts-a-function 123) 123

7.9 問題

7.9.1 合約和eq?

作為一般規則，向程式中添加一個合約既應該使程式的行為保持不變，也應該标志出一個合約違反。并且這對于Racket合約幾乎是真實的，隻有一個例外：eq?。

eq?過程被設計為快速且不提供太多的確定方式，除非它傳回true，這意味着這兩個值在所有方面都是相同的。在内部，這被實作為在一個底層的指針相等，是以它揭示了有關Racket如何被實作的資訊（以及合約如何被實作的資訊）。

用eq?進行合約互動是糟糕的，因為函數合約檢查被内部實作為包裝器函數。例如，考慮這個子產品：

#lang racket

(define (make-adder x)

(if (= 1 x)

add1

(lambda (y) (+ x y))))

(provide (contract-out

[make-adder (-> number? (-> number? number?))]))

除當它的輸入是1時它傳回Racket的add1外，它輸出通常被柯裡化為附加函數的make-adder函數。

你可能希望這樣：

(eq? (make-adder 1)

(make-adder 1))

應該傳回#t，但它卻沒有。如果該合約被改為any/c（或者甚至是(-> number?any/c)），那eq?調用将傳回#t。

教訓：不要對有合約的值使用eq?。

7.9.2 合約邊界和define/contract

被define/contract建立的合約邊界，它建立了一個嵌套的合約邊界，有時是不直覺的。當多個函數或其它帶有合約的值互相作用時尤其如此。例如，考慮這兩個互相作用的函數：

> (define/contract (f x)     (-> integer? integer?)     x)

> (define/contract (g)     (-> string?)     (f "not an integer"))

> (g)

f: contract violation

expected: integer?

given: "not an integer"

in: the 1st argument of

(-> integer? integer?)

contract from: (function f)

blaming: top-level

(assuming the contract is correct)

at: eval:2.0

人們可能期望這個函數g将因為違反其帶f的合約條件而被歸咎。如果f和g是直接建立合約的對方，歸咎于g就是對的。然而，它們不是。相反，f和g之間的通路是通過封閉子產品的頂層被協調的。

更确切地說，f和子產品的頂層有(-> integer? integer?)合約協調它們的互相作用，g和頂層有(-> string?)協調它們的互相作用，但是f和g之間沒有直接的合約，這意味着在g的主體内對f的引用實際上是子產品職責的頂層，而不是g的。換句話說，函數f已經被用在g與頂層之間沒有合約的方式賦予g，是以頂層被歸咎。

如果我們想在g和頂層之間增加一個合約，我們可以使用define/contract的#:freevar申明并看到預期的歸咎：

> (define/contract (f x)     (-> integer? integer?)     x)

> (define/contract (g)     (-> string?)     #:freevar f (-> integer? integer?)     (f "not an integer"))

> (g)

f: contract violation

expected: integer?

given: "not an integer"

in: the 1st argument of

(-> integer? integer?)

contract from: top-level

blaming: (function g)

(assuming the contract is correct)

at: eval:6.0

教訓：如果帶合約的兩個值應互相作用，在子產品邊界上将它們放置在具有合約的分開的子產品中或使用#:freevar。

7.9.3 存在的合約和判斷

很像上面的這個eq?例子，#:∃合約能夠改變一個程式的行為。

具體來說，null?判斷（和許多其它判斷）為#:∃合約傳回#f，同時那些合同中的一個改變為any/c意味着null?現在可能反而傳回#t，任何不同行為的結果依賴于這個布爾值可以怎樣在程式中流動。

#lang racket/exists

package: base

要解決上述問題，racket/exists庫行為就像racket，但當給定#:∃合約時判斷會發出錯誤信号。

教訓：不要使用基于#:∃合約的判斷，但是如果你并不确定，用racket/exists在是安全的。

7.9.4 定義遞歸合約

當定義一個自參考合約時，很自然地去使用define。例如，人們可能試圖在像這樣的流上編寫一個合約：

> (define stream/c     (promise/c      (or/c null?            (cons/c number? stream/c))))

stream/c: undefined;

cannot reference undefined identifier

不幸的是，這不會工作，因為stream/c的值在被定義之前就被需要。換句話說，所有的組合器都渴望對它們的參數求值，即使它們不接受這些值。

相反，使用

(define stream/c

(promise/c

(or/c

null?

(cons/c number? (recursive-contract stream/c)))))

recursive-contract的使用延遲對辨別符stream/c的求值，直到合約被首先檢查之後，足夠長以確定stream/c被定義。

也參見《檢查資料結構的特性》。

7.9.5 混合set!和contract-out

假定變量通過contract-out輸出的合約庫沒有被配置設定，但沒有執行它。是以，如果你試圖set!這些變量，你可能會感到驚訝。考慮下面的例子：

> (module server racket     (define (inc-x!) (set! x (+ x 1)))     (define x 0)     (provide (contract-out [inc-x! (-> void?)]                            [x integer?])))

> (module client racket     (require 'server)     (define (print-latest) (printf "x is ~s\n" x))     (print-latest)     (inc-x!)     (print-latest))

> (require 'client)

x is 0 x is 0

盡管x的值已經被增加（并且在子產品x内可見），兩個對print-latest的調用列印0。

為了解決這個問題，輸出通路器函數，而不是直接輸出變量，像這樣：

#lang racket

(define (get-x) x)

(define (inc-x!) (set! x (+ x 1)))

(define x 0)

(provide (contract-out [inc-x! (-> void?)]

[get-x (-> integer?)]))

教訓：這是一個我們将在一個以後版本中讨論的缺陷。