RFC: for loops #4

RustanLeino · 2021-01-21T00:52:09Z

No description provided.

samuelgruetter · 2021-01-21T01:23:14Z

for-loops.md

+``` dafny
+var _lo := lo;
+var _hi := hi;
+assert _lo <= _hi; // this is Dafny-like


What does // this is Dafny-like mean?

Do we really need to assert _lo <= _hi? This could be needlessly restrictive: I think there are some situations where lo might already be bigger than hi, and the intended behavior is simply to do no loop iterations at all if that's the case.

I definitely agree. It is really useful if the loop simply does nothing when lo > hi. Note: I understand it will do nothing when lo == hi, the interval being half-open.

I thought this would be "Dafny-like" because Dafny already imposes the restriction lo <= hi in an expression s[lo..hi].

What is an example when allowing lo > hi is useful? Is it a frequent occurrence?

I think lo == hi (which should result in 0 iterations) is very common, and lo > hi is less common, but here's an example: Say I write a method to resize an array from oldsize to newsize (and I don't know which one is bigger), and if newsize is bigger, the new elements should be initialized to some default value, so after copying the elements, maybe I want to be "smart" and write a loop like for i in [oldsize..newsize] { newarray[i] = default } and run that loop no matter whether oldsize or newsize is bigger, relying on the fact that if oldsize is bigger, 0 iterations will be performed. But I guess examples like this one can be easily rewritten so that they also work if lo <= hi is required by Dafny, I can't think of an example right now where such rewriting would be too cumbersome.

Thanks for the thoughts. For this particular example, one can also use a forall statement:

forall i | 0 <= i < newsize { newarray[i] := if i < oldsize then oldarray[i] else default; }

samuelgruetter · 2021-01-21T01:24:27Z

Did you consider making all for-loops iterator-based (like Python)?
This would allow using the same construct to iterate through collections as well as through ranges, and ranges could also specify a step size:

for i in myList.iterator()
  invariant J
{
  ...
}

// starts at 10, decrements by 2, as long as i > 0
for i in range(10, 0, -2)
{
  print(i);
}

backtracking · 2021-01-21T09:04:51Z

for-loops.md

+Two central design points are: 
+- the half-open interval of values for which the loop body is performed (e.g., `0 <= i < a.Length`) and
+ the closed interval that appears in the loop invariant (e.g., `0 <= i <= a.Length`)
+- what should be the possible increments of the loop index (e.g., `+1`, `-1`, `+2`)


In my opinion, increments other than +1 and -1 are a non-issue. It happens rarely and when it does, we simply use a while loop.

backtracking · 2021-01-21T09:24:54Z

for-loops.md

+}
+```
+
+is still available.


FYI, Why3 has a for each loop with syntax

for <pat> in <expr> with <Module> do invariant {...} variant {...} <body> done

It roughly desugars to

let it = <Module>.create <expr> in try while true do invariant {...} variant {...} let <pat> = <Module>.next it in <body> done with <Module>.Done -> () end

which means that <Module> is providing

a function create (to create the iterator from <expr>)

a function next (to get the next value)

an exception Done (to signal termination of the iteration)

Note: break and continue are honored.

Regarding the way to specify create and next, you might be interested in this NFM 2016 paper:
https://hal.inria.fr/hal-01281759v2/document

What is the reason not to use just foreach loops (using the for keyword seems fine)?

[lo .. hi] in for i in [lo .. hi] is already in Dafny. That'd allow for arbitrary stepping using sequence comprehensions such as in for x in seq(5, i => i*i).

The versions with just -1 and +1 updates seem restrictive to me.

RustanLeino · 2021-04-09T17:19:10Z

@samuelgruetter @backtracking @mschlaipfer I like the idea of also supporting a foreach loop. (I also really like the <pat> LHS in Why3 -- great idea!)

Dafny has CLU-style iterators. However, they are rarely used, because of some shortcomings. One shortcoming is that they are tricky to specify in general, though simple iterators are fairly easy to specify. Another shortcoming is that iterators don't have a common supertype (other than object). This would be useful to have. The most severe shortcoming is that there is no built-in foreach construct. This means users have to write a white loop of the correct form, and this requires knowing--even for simple iterators--about the various special fields that are there to support the general case. A built-in foreach loop could fix this.

(The Why3 use of exceptions as part of the foreach definition makes me think of Dafny's :-. Maybe there's something cool one can do here, but I don't see exactly what it is.)

The need has also come up for foreach loops over Dafny's built-in collection types (set, map, etc.). It would be nice to combine such a foreach loop with a foreach loop for user-defined iterators.

Finally, I don't know what reason Why3 had to have separate for and foreach loops, but I'm feeling some resistance to the idea of using foreach loops for everything. The automatically generated invariant is more complicated for foreach loops, so from a verification learning standpoint, I think the primitive nature of for is simpler. For example, if the foreach is over a set, like

foreach x in S {
  Body;
}

then you'd want something like this:

var tmpS := S;
var tmpDone := {};
while tmpDone != tmpS
  invariant tmpDone <= tmpS
  decreases |tmpS| - |tmpDone|
{
  var x :| tmpS - tmpDone;
  Body;
  tmpDone := tmpDone + {x};
}

There probably also needs to be some syntax for mentioning what I here called tmpDone.

So, I'm thinking for and foreach would be different statements. There's room for a RFC for a foreach.

backtracking · 2021-04-12T06:54:46Z

Finally, I don't know what reason Why3 had to have separate for and foreach loops, but I'm feeling some resistance to the idea of using foreach loops for everything.

Why3 has for and foreach for historical reasons: we had for long before we added foreach. Anyway, I would not make for a particular case of foreach (over an interval) as, as you said, this would complicate the loop invariant a lot. With a for loop, the invariant only depends on the loop index, an integer, which is at hand. It is named in tbe code. With a foreach loop, you have to refer to the sequence of the values already traversed / yet to be traversed (or both), and you have to provide a way to name them. Because of nested loop, you can't use fixed names for these sequences (such as done / todo for instance).

RustanLeino · 2021-04-12T22:17:59Z

Here's another question. For the most typical for loop (with a +1 increment), using

for i := 0 to 100

seems straightforward. But what about the -1 direction. Previously, I had thought of

for i := 100 downto 0

The order of the two bounds (100 and 0 in my example here) is suggestive of the order in which the iterations will be executed. But here's another choice:

for i := 0 from 100

Here, the lower/upper bounds are written in the same order as in the standard to (+1) case. This has the advantage that the inclusive bound is still on the left and the exclusive bound is on the right.

Is the 0 from 100 to be preferred over 100 downto 0?

backtracking · 2021-04-13T06:39:53Z

I definitely prefer the downto version, but I'm obviously influenced by almost 30 years of OCaml and the fact that we adopted the OCaml syntax in Why3.

By the way, here is a good use example of downto: in place heapsort.

let heapsort a =
  let n = Array.length a in
  for k = (n-2) / 2 downto 0 do downheap a k n done;
  for k = n-1 downto 1 do swap a 0 k; downheap a 0 k done

where downheap a i hi moves a[i] down in the heap using hi as (exclusive) upper limit.

Note that, when n is 0 (empty array),

the first loop goes from -1 to 0 and thus does nothing;
the second loop goes from -1 to 1 and thus does nothing. This is an example of a 2-gap by the way.

samuelgruetter · 2021-04-13T15:02:17Z

0 from 100 looks a bit unintuitive to me. A more intuitive but also more verbose option might be 0 to 100 backwards.

RustanLeino added 2 commits January 20, 2021 16:40

RFC: for loops

252a02b

Little edits

2bb025c

RustanLeino mentioned this pull request Jan 21, 2021

feature request: for loops dafny-lang/dafny#7

Closed

samuelgruetter reviewed Jan 21, 2021

View reviewed changes

backtracking reviewed Jan 21, 2021

View reviewed changes

RustanLeino mentioned this pull request Jun 30, 2021

For loops dafny-lang/dafny#1264

Merged

RustanLeino closed this in dafny-lang/dafny#1264 Jul 2, 2021

robin-aws mentioned this pull request Feb 1, 2022

Design Proposal: Support for enumeration dafny-lang/dafny#1753

Open

robin-aws mentioned this pull request Mar 31, 2022

foreach loops and sequence comprehensions #9

Closed

robin-aws mentioned this pull request May 12, 2022

Ordered quantification (foreach loops and sequence comprehensions - take 2) #10

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

RFC: for loops #4

RFC: for loops #4

RustanLeino commented Jan 21, 2021

samuelgruetter Jan 21, 2021

backtracking Jan 21, 2021

RustanLeino Apr 9, 2021

RustanLeino Apr 9, 2021

samuelgruetter Apr 9, 2021

RustanLeino Apr 12, 2021 •

edited

Loading

samuelgruetter commented Jan 21, 2021

backtracking Jan 21, 2021

backtracking Jan 21, 2021 •

edited

Loading

backtracking Jan 21, 2021

mschlaipfer Apr 8, 2021

RustanLeino commented Apr 9, 2021

backtracking commented Apr 12, 2021

RustanLeino commented Apr 12, 2021

backtracking commented Apr 13, 2021 •

edited

Loading

samuelgruetter commented Apr 13, 2021

RFC: for loops #4

RFC: for loops #4

Conversation

RustanLeino commented Jan 21, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RustanLeino Apr 12, 2021 • edited Loading

Choose a reason for hiding this comment

samuelgruetter commented Jan 21, 2021

Choose a reason for hiding this comment

backtracking Jan 21, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RustanLeino commented Apr 9, 2021

backtracking commented Apr 12, 2021

RustanLeino commented Apr 12, 2021

backtracking commented Apr 13, 2021 • edited Loading

samuelgruetter commented Apr 13, 2021

RustanLeino Apr 12, 2021 •

edited

Loading

backtracking Jan 21, 2021 •

edited

Loading

backtracking commented Apr 13, 2021 •

edited

Loading