スキームの契約違反がありません

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の入力でどのように契約が本当に戻ってきたかはわかりません。

EDIT：明確にするために、私は契約を違反させる方法を探していません。私はすでに私が/ cを使用できることを知っています（@ soegaardのおかげで）私はpositive?とinteger?を改めることができます。私がここで探しているのは、ここで何が起こっているのかを理解することです。

ありがとうございました！

Answer 1

UPDATE

私は完全にあなたがあなたの例では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 

SECOND UPDATEここ

は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?))と同じ働きをしていることにも注意してください。コードで

：あなたは私たちは異なるアプローチを必要とする両方のc1とc2を使用する契約を締結したいので

(and c1 c2) 

が

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

と同じです。 2つの述語を単純述語に結合する方法を調べてみましょう。ない述語自身に -

(and/p p1 p2) 

は述語によって返された値に使用されている。ここ

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

andのために短くする必要があります。

コンストラクトand/cはand/pと同様に機能しますが、コントラクトの表現は述語よりも複雑です。しかし、原則は同じです。

は

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