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))))))