Home My Page Projects The Why platform
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

[#5491] [Jessie] normalization of *for* loops with multiple updates

Date:
2008-04-22 14:26
Priority:
3
State:
Open
Submitted by:
Nicolas Rousset (nrousset)
Assigned to:
Nobody (None)
Hardware:
none
Product:
none
Operating System:
none
Component:
none
Version:
none
Severity:
none
Resolution:
none
URL:
Summary:
[Jessie] normalization of *for* loops with multiple updates

Detailed description
The following example, with 2 updates in the for loop (i++ and n = i) :

unit f() {
var integer i = 0;
var integer n = 0;
for (; (i < 10) ; (i ++), (n = i)) { () }
}

produces the following 'wrong' normalized expression with the second update in position of the loop invariant(!), and jessie (CVS version) eventually fails to type this expression :

$ jessie Loops.jc
Normalized expression:
{
(let integer i = 0 in
{
(let integer n = 0 in
{
{
(try loop
invariant (n = i);
(try {
(TODO if); (throw Loop_continue ())
} with
| Loop_continue jessie_3 -> {
true;
(let jessie_1 = i in { (i = (jessie_1 + 1)); jessie_1 })
}
| default -> ()) done with
| Loop_exit jessie_2 -> ()
| default -> ())
}
})
})
}

File "Loops.jc", line 5, characters 29-34: typing error: construction not allowed in logic assertions

No Comments Have Been Posted

No Changes Have Been Made to This Item