The response property is the most commonly used in formal software verification. Response(p; q) is true if every

time p holds, it is followed by q. Formally, Response(p; q) is true iff ∀ moments of time (states) i, if p(i) (meaning p

holds at moment i) then ∃ j ≥ i and q(j).

Write an ACL2 function (response qp) that takes a list of characters and returns T if the above relation is satisfied, and

returns nil if p holds at some moment and is not followed by q at a later moment.

In your modeling of the list, use the notation (a b) to indicate that a and b hold at the same moment. For exam-

ple, in the list ’(a b (c d) e), a holds at moment 1, b at moment 2, c and d at moment 3, and e at moment 4.

Possible cases to test your function against are:

• (response qp (a b c d)) returns T.

• (response qp (a b q d)) returns T.

• (response qp (a b p q)) returns T.

• (response qp (a b (p q) d)) returns T.

• (response qp (a b q q p)) returns Nil.

Here is what I have

- Code: Select all
`(DEFUN RESPONSE_qp (p q)`

(COND ((consp p)(cdr q))

((listp p) (response_qp(car q) p))

(t (response_qp (p) (response_qp( q))))))

Thanks