[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Liberty-eiffel] locals in postcondition
From: |
Raphael Mack |
Subject: |
[Liberty-eiffel] locals in postcondition |
Date: |
Wed, 27 Aug 2014 20:12:18 +0000 |
User-agent: |
Internet Messaging Program (IMP) H5 (6.2.1) |
Hello all,
is it allowed to access locals in a postcondition? I don't think it
makes much sense...
If we have a closure in the postcondition we get warnings about using
the same variable names:
add_instructions (a_instructions: TRAVERSABLE[INSTRUCTION])
local
i: INTEGER
do
i := 3
ensure
added_last_in_reverse_order: (create {ZIP[INSTRUCTION,
INTEGER]}.make(a_instructions,
1 |..| a_instructions.count)
).for_all(agent (inst:
INSTRUCTION; i: INTEGER): BOOLEAN
do
Result := inst =
instructions_list.item(instructions_list.upper - i + 1)
end)
end
is this what we want?
Rapha
- [Liberty-eiffel] locals in postcondition,
Raphael Mack <=