 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| • |
Once
the simulator is proved correct, we can prove
|
|
|
properties
of specifications w.r.t. the simulator
|
|
|
| • |
Our protocol is correct if sender and receiver agree on the
|
|
|
id
of the last successfully transmitted frame
|
|
|
(defthm sender-receiver-agree-1
|
|
|
(<= (variable-value
'ackid
|
|
|
(instance 'receiver (simulate S O)))
|
|
|
(variable-value
'frameid
|
|
|
(instance 'sender (simulate
S O)))))
|
|
|
(defthm sender-receiver-agree-2
|
|
|
(let ((v1 (variable-value
|
|
|
'ackid (instance
'receiver (simulate S O))))
|
|
|
(v2
(variable-value
|
|
|
'frameid (instance 'sender (simulate S
O)))))
|
|
|
(implies (< v1 v2)
(= (+ 1 v1) v2))))
|
|
|
| • |
Defined access functions to extract variables and instances
|