Я пытался выяснить, как заставить работать постусловие для следующего кода. Есть 3 класса, Банк является клиентом Клиента, а Клиент является клиентом Счета.
Вот класс банка, я просто не могу передать постусловие other_customer_unchanged
new (name1: STRING)
-- Add a new customer named 'name1'
-- to the end of list `customers'
require
customer_not_already_present:customer_exists(name1)=false
do
customers.force (create {CUSTOMER}.make (name1))
count := customers.count
ensure
total_balance_unchanged:
sum_of_all_balances = old sum_of_all_balances
num_customers_increased:count /= old count and old count+1=count
total_unchanged:total = old total
customer_added_to_list:
customer_exists (name1)
and then customers[customer_id (name1)].name ~ name1
and then customers[customer_id (name1)].balance ~ zero
other_customers_unchanged:
customers_unchanged_other_than(name1, old customers.deep_twin)
end
Вот особенность customers_unchanged_other_than
customers_unchanged_other_than (a_name: STRING;old_customers:like customers): BOOLEAN
-- Are customers other than `a_name' unchanged?
local
c_name: STRING
do
from
Result := true
customers.start
until
customers.after or not Result
loop
c_name := customers.item.name
if c_name /~ a_name then
Result := Result and then
old_customers.has (customers.item)
end
customers.forth
end
ensure
Result =
across
customers as c
all
c.item.name /~ a_name IMPLIES
old_customers.has (c.item)
end
end
и я переопределил функцию is_equal в классе клиентов
is_equal (other: like Current): BOOLEAN
do
Result := name ~ other.name and balance = other.balance
ensure then
Result = (name ~ other.name and balance = other.balance)
end
Я изучил, что находится в старом файле customer.deep_twin, он содержит элемент клиента, но каким-то образом, когда он использует функцию .has, он просто делает результат ложным. Любая помощь приветствуется :)
