未违反计划合同

Question

首先，对于初学者的问题，我深表歉意。我是一位经验丰富的开发人员，但对 Scheme 还是个新手。我创建了一个需要正整数的合约，但是当我提供一个实数时，合约没有被违反：

(define/contract (listofOne n)
  (-> (and integer? positive?) (listof integer?))
  (cond
    ((= n 0) '())
    (else (cons 1 (listofOne (- n 1))))))

(listofOne 12.5)

我预计合同会被违反，但我却遇到了无限循环和缓冲区溢出。为什么契约没有被违反？我的谓词中的第一个查询是 integer?，所以我看不出合同如何通过输入 12.5.

返回 true

编辑： 澄清一下，我不是在寻找违反合同的方法。我已经知道我可以使用 and/c，并且（感谢@soegaard）我可以反转 positive? 和 integer? 来违反它。我现在正在寻找的是了解这里发生的事情。

在此先感谢您的帮助！

Answer 1

更新

我完全没有注意到您在示例中使用了 and 而不是 and/c。试试这个：

#lang racket
(define/contract (listofOne n)
  (-> (and/c integer? positive?) (listof integer?))
  (cond
    ((= n 0) '())
    (else (cons 1 (listofOne (- n 1))))))

(listofOne 12.5)

结果：

listofOne: contract violation
  expected: integer?
  given: 12.5
  in: an and/c case of
      the 1st argument of
      (->
       (and/c integer? positive?)
       (listof integer?))
  contract from: (function listofOne)
  blaming: anonymous-module
   (assuming the contract is correct)
  at: unsaved-editor:2.18

第二次更新

这里是and的解释。

形式

(and c1 c2)

表示：

1. Evaluate `c1` giving a value `v`
2. If the value `v1` is false, 
   then the result of the `and`-expression is false.
   (note that `c2` is not evaluated)
3. If the value `v1` is non-false, 
   then evaluate the expression `c2` giving a value `v2`.
4. The result of the and-expressions is v2.

注意：如果 c1 的计算结果为真，则 (and c1 c2) 给出与 c2 相同的结果。这特别意味着如果 c1 是一个合同（这是一个非假值）然后 (and c1 c2) 给出与 c2.

相同的结果

在您的示例中 (and integer? positive?) 给出与 positive? 相同的结果。

另请注意，这意味着 (-> (and integer? positive?) (listof integer?)) 与 (-> positive? (listof integer?)) 的工作方式相同。

在代码中：

(and c1 c2)

与

相同

(let ([v1 c1])
  (if v1
      (let ([v2 c2])
         v2)
      #f))

由于您想要一个同时使用 c1 和 c2 的合同，我们需要一种不同的方法。让我们看看如何将两个谓词组合成一个简单的谓词。

(and/p p1 p2)

应该是

的缩写

(lambda (x)
  (and (p1 x) (p2 x)))

此处 and 用于谓词返回的值 - 而不是谓词本身。

构造 and/c 的工作方式与 and/p 类似，但合同的表示比谓词更复杂。原理是一样的。

是

的缩写

(let ([t c1])
  (if t
      t
      c2))

未违反计划合同

Scheme contract not violated

scheme

racket

contract