* FOR Iteration Scheme
@ 1988-07-18 20:15 Richard Pattis
1988-07-19 20:43 ` David E. Emery
0 siblings, 1 reply; 3+ messages in thread
From: Richard Pattis @ 1988-07-18 20:15 UTC (permalink / raw)
In the process of writing a CS-1 book that uses Ada as its langauge of
discourse, I am trying to describe formally the semantics of the FOR iteration
scheme using other parts of Ada (whose semantics I explain operationally). Is
the following the most accurate statement I can make? CAUTION: I am in the
process of learning Ada (trying to compose such explanations helps me), so
this may be a naive question.
FOR I IN E1..E2 LOOP
<body>
END LOOP;
is equivalent to the following code fragment, where the values of E1 and E2
share subtype <Type-Mark> and <ub> and <is> are secret objects generated by
the Ada compiler.
DECLARE
<is> : <Type-Mark> := E1;
<ub> : CONSTANT <Type-Mark> := E2;
BEGIN
IF <is> <= <ub>
THEN
LOOP
DECLARE
I : <Type-Mark> CONSTANT := <is>;
BEGIN
<body>
END;
EXIT WHEN <is> = <ub>;
<is>:= <Type-Mark>'SUCC(<is>);
END LOOP;
END IF;
END;
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: FOR Iteration Scheme
@ 1988-07-19 13:52 John.Goodenough
0 siblings, 0 replies; 3+ messages in thread
From: John.Goodenough @ 1988-07-19 13:52 UTC (permalink / raw)
Such code fragments never seem to be completely equivalent. Your structure is
not equivalent for expanded names, e.g., PROC.LOOP_NAME.I, won't be possible
because you've introduced an extra level of declare block.
In addition, language commentary AI-00006 says that the subtype of the loop
parameter is determined by the discrete range of the loop. "In particular, if
the discrete range is static, the loop parameter has a static subtype". This
affects the legality of case statements:
for J in 1..2 loop
case J is
when 1 => ... ;
when 2 => ...;
end case;
No other choices are allowed or required.
Also, your equivalence should emphasize that the loop parameter is defined by
a base type:
type T is range 0..255;
for I in T'BASE'FIRST..T'PRED(T'FIRST) loop
-- no exception and no positive values!
So, your equivalence should be:
DECLARE
<lb> : CONSTANT <Base-Type-Mark> := E1;
<is> : <Base-Type-Mark> := <lb>;
<ub> : CONSTANT <Base-Type-Mark> := E2;
BEGIN
IF <is> <= <ub>
THEN
LOOP
DECLARE
I : CONSTANT <Base-Type-Mark> RANGE <lb> .. <ub> := <is>;
BEGIN
<body>
END;
EXIT WHEN <is> = <ub>;
<is>:= <Type-Mark>'SUCC(<is>);
END LOOP;
END IF;
END;
The initialization of I with <is> ensures that I cannot be used in a static
expression, since it is not a static constant.
Having had bad luck with trying to define such equivalences, it wouldn't
surprise me if there is something else wrong with the above equivalence (apart
from the expanded name problem). Any such problem will almost certainly have
to do with interactions with other rules in the language, and not the semantic
behavior of the loop.
John B. Goodenough (Goodenough@sei.cmu.edu)
Software Engineering Institute
Pittsburgh, PA 15213
412-268-6391
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: FOR Iteration Scheme
1988-07-18 20:15 FOR Iteration Scheme Richard Pattis
@ 1988-07-19 20:43 ` David E. Emery
0 siblings, 0 replies; 3+ messages in thread
From: David E. Emery @ 1988-07-19 20:43 UTC (permalink / raw)
>From: pattis@june.cs.washington.edu (Richard Pattis)
> In the process of writing a CS-1 book that uses Ada as its langauge of
>discourse, I am trying to describe formally the semantics of the FOR iteration
>scheme using other parts of Ada (whose semantics I explain operationally). Is
>the following the most accurate statement I can make? CAUTION: I am in the
>process of learning Ada (trying to compose such explanations helps me), so
>this may be a naive question.
This might also be a naive question: Why are you writing a book about
a language you do not know?
Didn't the Boehm-Jacobini proof demonstrate the semantics of FOR loops
using iteration and selection?
dave emery
emery@mitre-bedford.arpa
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~1988-07-19 20:43 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1988-07-18 20:15 FOR Iteration Scheme Richard Pattis
1988-07-19 20:43 ` David E. Emery
-- strict thread matches above, loose matches on Subject: below --
1988-07-19 13:52 John.Goodenough
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox