Added precondition to WSF_FILTER.set_next (..) to avoid cycle.

This commit is contained in:
Jocelyn Fiat
2017-04-13 22:55:39 +02:00
parent 4eb743fa58
commit a57e041003

View File

@@ -29,6 +29,8 @@ feature -- Element change
set_next (a_next: like next)
-- Set `next' to `a_next'
require
a_next_is_not_current: a_next /= Current
do
next := a_next
ensure