lisp-“汽车：预期违反合同：对？给定：()”同时在访问控制模型中销毁 obj答案

【问题标题】：lisp-"car: contract violation expected: pair? given: ()" while destroy an obj in an access control modellisp-“汽车：预期违反合同：对？给定：()”同时在访问控制模型中销毁 obj
【发布时间】：2018-02-04 16:32:15
【问题描述】：

编写一个程序来销毁我的访问控制模型中的对象并模拟每种情况。这是我的代码。

 (define st1 (term (st 3 2 (,s0 ,s1 ,s2) (,o0 ,o1) ,br ,m1)))
 (define m1 (term ((,s0 control ,s0) (,s1 (trans ,r1) ,o0) (,s2 ,r2 ,o1))))
 (define r1 (term read))
 (define r2 (term write))
 (define br (term (,r1 ,r2)))
 (define-language GD 
 [Sub   (sub natural)]
 [PObj  (obj natural)]
 [Obj   Sub
     PObj]
 [AR    own
     control]
  [BR    (variable-except own control)]
  [TR    (trans BR)]
  [Right BR
     AR
     TR]
  [Priv  (Sub Right Obj)]
  [S     (Root Sub ...)]
  [O     (PObj ...)]
  [R     (BR ...)]
  [M     (Priv ...)]
  [State (st natural natural S O R M)]
  [Root  (sub 0)]
)

 (define s1 (term (sub 1)))
 (define s2 (term (sub 2)))
  (define s0 (term (sub 0)))

 (define o0 (term (obj 0)))
  (define o1 (term (obj 1)))
 (define o2 (term (obj 2)))
 (define o3 (term (obj 3)))

这是测试代码。

   (define red1
  (reduction-relation
   GD
   (--> (st natural_1 natural_2
        S (PObj_0 ... PObj_2 PObj_4 ...)
        R M_1)
    (st natural_1 ,(- (term natural_2) 1)
        S (PObj_0 ... PObj_4 ...)
        R M_2)
    (where (PObj_1 ... PObj_2 PObj_3 ...) (PObj_0 ... PObj_2 PObj_4 ...))
    (where M_2 ,(destroy-Obj (term (PObj_2)) (term M_1)))
    (computed-name (term (destroy PObj_2))))
   )
  )

(define (destroy-Obj Obj matrix)
  (let ([o1 (third (car matrix))])
(cond
[(eqv? (first Obj) 'obj)
 (cond
   [(eqv? o1 Obj) destroy-Obj Obj (cdr matrix)]
   [else (cons (car matrix) (destroy-Obj Obj (cdr matrix)))])]

[else (cons (car matrix) (destroy-Obj Obj (cdr matrix)))])))

当我想销毁 st1 中的一个对象时。我这样测试：

(stepper red1 st1)

我不断收到此错误：

car: contract violation
  expected: pair?
  given: ()

“矩阵”是我要销毁包括“Obj”在内的任何列表的矩阵。 “Obj”可以是 o1 或 o2。我将“M_1”放入矩阵。我想将“st1”的“m1”放入“M_1” “m1”已被定义。它不应该是空的。那么为什么会发生这个错误呢？非常感谢！！

【问题讨论】：

标签： scheme plt-redex

【解决方案1】：

通过查看您所做的代码(third (car matrix)) 并在递归步骤中(destroy-Obj Obj (cdr matrix)) 暗示matrix 最终将不是一对。因此，您的代码需要处理matrix 不是一对的事件，或者更具体的()（如果这是有保证的替代方案）（我的事件matrix 始终是一个正确的列表）。

我还注意到(eqv? o1 Obj) 是(begin destroy-Obj Obj (cdr matrix)) 的结果，这与(cdr matrix) 相同（cond 术语后果/替代具有明确的begin）。也许你没有括号，所以你的意思是(destroy-Obj Obj (cdr matrix))。

【讨论】：