【问题标题】:Scheme contract not violated未违反计划合同
【发布时间】:2016-10-21 18:37:54
【问题描述】:

首先,我为初学者的问题道歉。我是一位经验丰富的开发人员,但对 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? 以使其违反。我现在正在寻找的是了解这里发生了什么。

提前感谢您的帮助!

【问题讨论】:

    标签: scheme racket contract


    【解决方案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))
    

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

    (and/p p1 p2)
    

    应该简称

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

    这里and 用于谓词返回的值,而不是谓词本身。

    and/c 的构造类似于and/p,但合约的表示比谓词更复杂。原理是一样的。

    简称

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

    【讨论】:

    • and/c 是否越界?我与和/c 违反合同。我已经阅读了大约 10 次 and/c 的解释,但我仍然不明白它的作用。
    • 对不起!我错过了你在合同中使用and 而不是and/c
    • 我看到它可以与 and/c 一起使用,但是……为什么?为什么它不适用于and,但它适用于and/c?
    • 好吧,and 适用于表达式,and/c 适用于合同。唔。让我们看看如果我们使用and 会发生什么。在(and c1 c2) 中,c1c2 计算为合约,因为and 是“短路”,我们有(and c1 c2) 计算为c1 的值。合同c2 因此被忽略。另一方面,构造 and/c 检查两个合同并检查两个合同是否都已履行。
    • @soegaard and 应该只能在#f 上短路,而不是在#t 上。 en.wikipedia.org/wiki/Short-circuit_evaluation
    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 2016-08-30
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 2016-03-19
    相关资源
    最近更新 更多