<no subject>
Author Message
<no subject>

I search for the variant and invariant of
a simple for-loop?

--
GMX - Die Kommunikationsplattform im Internet.
http://www.*-*-*.com/

--
Posted from mx0.gmx.net [213.165.64.100]
via Mailgate.ORG Server - http://www.*-*-*.com/

Fri, 10 Oct 2003 00:39:52 GMT
<no subject>

Quote:

>I search for the variant and invariant of
>a simple for-loop?

FOR loops are supported in Oberon-2, but not in Oberon proper.  The reason
is that a FOR loop is really just syntactic sugar for a WHILE loop.
Consider the following:

VAR
x: ARRAY 10 OF CHAR;
i: INTEGER;

BEGIN
FOR i = 0 TO 9 DO
x[i] := i
END
END;

We can rewrite this using a WHILE loop:

VAR
x: ARRAY 10 OF CHAR;
i: INTEGER;

BEGIN
i := 0;
WHILE i < 10 DO
x[i] := i;
i := i + 1
END
END;

Not that much bigger or verbose, and almost always easier to understand
because it's more explicit.

--
KC5TJA/6, DM13, QRP-L #1447
Samuel A. Falvo II
Oceanside, CA

Fri, 10 Oct 2003 12:01:34 GMT
<no subject>

Quote:

> I search for the variant and invariant of
> a simple for-loop?

Hello!

In Ingo Dittmers "Konstruktion guter Algorithmen" I found the
following

{(a <=x<=e) and P([a...x-1])} S {P([a...x])}
-----------------------------
{P([{}])} FOR x:=a TO e DO S END {P([a...e])}

S is the statementsequence within the for-loop.
When you proved that P([a...x]) holds when you execute S
after (a <=x<=e) and P([a...x-1]) holds, with the above rule it
is proven that P([a...e]) holds after the for-loop when
P([{}]) holds before. The author notes that nothing is said
about the value of x after the loop.

I hope this helps you. If you need more information I can
find out other books e.g.

Greetings,
Marco

Sun, 12 Oct 2003 03:47:45 GMT
<no subject>
"Samuel A. Falvo II" schreef:

Quote:

> >I search for the variant and invariant of
> >a simple for-loop?

> FOR loops are supported in Oberon-2, but not in Oberon proper.  The reason
> is that a FOR loop is really just syntactic sugar for a WHILE loop.
> Consider the following:

> VAR
>   x: ARRAY 10 OF CHAR;
>   i: INTEGER;

> BEGIN
>   FOR i = 0 TO 9 DO
>     x[i] := i
>   END
> END;

> We can rewrite this using a WHILE loop:

> VAR
>   x: ARRAY 10 OF CHAR;
>   i: INTEGER;

> BEGIN
>   i := 0;
>   WHILE i < 10 DO
>     x[i] := i;
>     i := i + 1
>   END
> END;

> Not that much bigger or verbose, and almost always easier to understand
> because it's more explicit.

And almost always easier to get wrong due to a fence post error.

The problem with this example is that the transcription is simple for
toy-like examples like the one above. However, when the for-loop gets
more complex, the simplicity of its while-based transcription
evaporates.

If explicitness is the primary design criterion, one better switch to
assembly language anyway.

--

Groeten, Karel Th?nissen

Hello Technologies develops high-integrity software for complex systems

Wed, 03 Dec 2003 18:08:11 GMT
<no subject>

Quote:

>> Not that much bigger or verbose, and almost always easier to understand
>> because it's more explicit.

>And almost always easier to get wrong due to a fence post error.

10 years and counting, and I never had a problem yet.

Quote:
>The problem with this example is that the transcription is simple for
>toy-like examples like the one above. However, when the for-loop gets
>more complex, the simplicity of its while-based transcription
>evaporates.

A laughable assertion.  If you really have that complicated a loop
structure, that's all the more reason not to use a FOR loop.

Quote:
>If explicitness is the primary design criterion, one better switch to
>assembly language anyway.

If I had a nickel for every time I heard this argument...

--
KC5TJA/6, DM13, QRP-L #1447
Samuel A. Falvo II
Oceanside, CA

Fri, 05 Dec 2003 07:19:01 GMT

 Page 1 of 1 [ 5 post ]

Relevant Pages