adding Merge Sort and Binary Search #49

prvshah51 · 2022-08-11T22:12:45Z

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

robin-aws

Great start! Here are some top-level suggestions (which will make some of the inline comments I made moot, but I added those anyway just for the sake of learning).

This code should be under src rather than examples - the latter is for sample uses of the actual functions/methods. I would suggest src/Collections/Arrays/Arrays.dfy to align with the established layout. The additional total ordering predicates on compare would fit nicely into the existing src/Functions.dfy file.
For sorting, I think proving HeapSort correct will take quite a bit of work. Why not steal the MergeSort implementation I did for the report generator instead? https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38 It definitely won't be as efficient given that it creates lots of intermediate subsequences (especially since most runtimes implement that as a copy instead of a reference), but it's already proven correct, and having that sorting algorithm here will still be an improvement over not having any sorting algorithm. :) You'll just have to replace calls to f(x) < f(y) with compare(x, y) just as you already have in BinarySearch.

robin-aws · 2022-08-11T22:22:36Z

examples/BinarySearch.dfy

+
+
+
+method BinarySearch<T>(a: array<T>, key: T,compare: (T, T) -> bool) returns (r: int)


I think it would be better to return an Option<nat> instead, so we don't have to use -1 as a special flag value.

robin-aws · 2022-08-11T22:23:54Z

examples/sorting.dfy

+      var temp:= a[0];
+      a[0]:= a[i];
+      a[i]:= temp;


Suggested change

var temp:= a[0];

a[0]:= a[i];

a[i]:= temp;

a[0], a[i] := a[i], a[0];

robin-aws · 2022-08-11T22:24:46Z

examples/sorting.dfy

+// Implemetation of Heap sort
+include "../src/Collections/Sequences/Seq.dfy"
+
+method SortArray<T>(a: array<T>, compare: (T, T) -> bool)


I'd name this HeapSortArray to be more precise, since there are other ways to sort (and may even be more in this repo in the future)

robin-aws · 2022-08-11T22:31:54Z

examples/BinarySearch.dfy

+
+
+method BinarySearch<T>(a: array<T>, key: T,compare: (T, T) -> bool) returns (r: int)
+  requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i],a[j])


You're missing the pre-conditions that ensure compare is a total ordering, which is why some of the assertions about correctness aren't verifying. You should be able to copy them here with proper attribution (I know all of the authors on that file would be happy to have their code in this repo :) - https://github.com/aws/aws-encryption-sdk-dafny/blob/mainline/src/Util/Sorting.dfy#L126-L127

You'll need exactly the same requires clauses on the sorting methods too.

robin-aws · 2022-08-11T22:33:49Z

examples/sorting.dfy

+include "../src/Collections/Sequences/Seq.dfy"
+
+method SortArray<T>(a: array<T>, compare: (T, T) -> bool)
+  requires multiset(a[..]) == multiset(old(a[..]))


This needs to be an ensures instead - it's describing the state of the array AFTER executing the method.

atomb · 2022-08-16T20:54:42Z

src/Collections/Sequences/Sorting.dfy

+  {}
+
+function method MergeSortBy<T>(a: seq<T>, compare: (T, T) -> bool ): (result :seq<T>)
+    ensures multiset(a) == multiset(result)


You also probably need a postcondition that the result is sorted.

In order to add SortedBy in a postcondition here, you'll need to export it from the module, as well.

And I think you'll also need these preconditions:

requires StandardLibrary.Transitive(compare) requires Connected(compare)

src/Collections/Sequences/Sorting.dfy

atomb · 2022-08-16T20:55:29Z

src/Collections/Sequences/Sorting.dfy

+    requires StandardLibrary.Transitive(compare)
+    requires Connected(compare)
+ { 
+    MergeSortBy(s,compare)


Because Sort is a method, you'll need something like result := MergeSortBy(s, compare);.

atomb · 2022-08-16T22:19:05Z

src/Collections/Arrays/BinarySearch.dfy

+  }
+
+method BinarySearch<T>(a: array<T>, key: T,compare: (T, T) -> bool) returns (r : nat)
+  requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i], a[j])


You might want to do this to allow the array to contain duplicates.

Suggested change

requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i], a[j])

requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i], a[j]) || a[i] == a[j]

atomb · 2022-08-16T22:20:05Z

src/Collections/Arrays/BinarySearch.dfy

+  ensures 0 <= r ==> r < a.Length && a[r] == key
+  ensures r < 0 ==> key !in a[..]
+  requires StandardLibrary.Transitive(compare)
+  requires Connected(compare)


I think this method requires an even more obscure property of the compare function. :)

requires StandardLibrary.Trichotomous(compare)

And it turns out that if you have that precondition you don't need Transitive or Connected.

src/Collections/Arrays/BinarySearch.dfy

atomb · 2022-08-16T22:22:11Z

src/Collections/Arrays/BinarySearch.dfy

+  {
+  }
+
+method BinarySearch<T>(a: array<T>, key: T,compare: (T, T) -> bool) returns (r : nat)


The way the spec is written right now, this method should return int instead of nat, though making it return Option<nat> might be even nicer, as I mention below.

atomb

Looks nice! I just suggested a few small changes for consistency and removal of duplication.

Eventually, I suspect we should split up StandardLibrary.dfy to put some of its contents in the more specialized modules that already exist (and maybe some new ones). For now, though, this at least makes a bunch more definitions available.

atomb · 2022-08-17T19:16:38Z

src/Collections/Arrays/BinarySearch.dfy

+
+
+
+module BinarySearch{


Suggested change

module BinarySearch{

module BinarySearch {

atomb · 2022-08-17T19:17:13Z

src/Collections/Arrays/BinarySearch.dfy

+  import opened Wrappers = StandardLibrary.Wrappers
+
+
+predicate Reflexive<T(!new)>(R: (T, T) -> bool) {


Suggested change

predicate Reflexive<T(!new)>(R: (T, T) -> bool) {

predicate Reflexive<T(!new)>(R: (T, T) -> bool) {

And I'd suggest similar changes throughout this file to ensure the indentation is consistent.

atomb · 2022-08-17T19:18:07Z

src/Collections/Sequences/Sorting.dfy

+include "../../UInt.dfy"
+include "../Sequences/Seq.dfy"
+
+module sorting{


Suggested change

module sorting{

module Sorting {

atomb · 2022-08-17T19:19:01Z

src/Collections/Sequences/Sorting.dfy

+  import opened UInt = StandardLibrary.UInt
+  import opened Seq
+
+predicate Reflexive<T(!new)>(R: (T, T) -> bool) {


This predicate and a bunch of those after it are duplicated between here and the BinarySearch module. Maybe they should go in StandardLibrary.dfy until we reorganize it to split it up a little more?

atomb · 2022-08-17T21:08:18Z

src/UInt.dfy

+
+module StandardLibrary.UInt {
+
+  // TODO: Depend on types defined in dafny-lang/libraries instead


This comment probably isn't needed anymore. :)

atomb · 2022-08-17T21:09:31Z

src/Collections/Arrays/BinarySearch.dfy

+
+module BinarySearch {
+  export
+    provides StandardLibrary, UInt


You'll probably want provides BinarySearch, too, so that people can use it.

atomb · 2022-08-17T21:10:07Z

src/Collections/Arrays/BinarySearch.dfy

+  import opened UInt = StandardLibrary.UInt
+  import opened Wrappers = StandardLibrary.Wrappers
+
+method BinarySearch<T>(a: array<T>, key: T, compare: (T, T) -> bool) returns (r:Option<nat>)


It'd be nice to have this indented two spaces to be consistent with the imports above it.

atomb

Nicely done!

I believe your comments have been addressed and that you'd prefer to have this merged sooner than later. :)

# Conflicts: # src/Collections/Sequences/Seq.dfy

The latter doesn’t work well in CI here because the /verificationLogger options cause extra, unpredictable output lines

robin-aws · 2022-09-13T21:32:48Z

@prvshah51 I've pushed several commits to remove more code we don't need (yet!), and made a few other changes to get it ready to merge IMO:

After discussion with @atomb I've removed Comparison.dfy and stuck to plain old (T, T) -> bool relations, which simplifies things for now.
Moved Relations.dfy to the top-level src directory (since we also have Functions.dfy there already)
Added an example that sorts and then searches, which also revealed that the "sorted" precondition on BinarySearch wasn't correct!

Let me know if you have any concerns, and @atomb / @MikaelMayer I'll leave it to you two to approve since I feel a little biased now that I've thrown my own commits on this. :)

Addressed own suggestions, recusing myself as biased :)

robin-aws · 2022-09-14T16:21:36Z

@MikaelMayer I just noticed you had some style requests that were lost in the shuffle. I'll respond to the ones I see that still seem relevant, but please just provide a quick comment at the top level if there are others we missed.

Re: the naming convention for predicates, e.g. "IsTotalOrder" instead of "TotalOrder", that's potentially a good idea but the latter convention is already established here in predicates like Functions.Injective. I'd suggest if you still feel strongly about it that you cut a repo issue for discussion, similar to #47.

Re: "lessThan" instead of "less", I don't have a strong opinion so I'd be willing to change it, personally. @prvshah51?

prvshah51 · 2022-09-14T16:43:14Z

Re: "lessThan" instead of "less", I don't have a strong opinion so I'd be willing to change it, personally. @prvshah51?

Both options are fine with me.

MikaelMayer · 2022-09-14T17:31:40Z

src/Collections/Sequences/MergeSort.dfy

+  import opened Relations
+
+  //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedWith`
+  function method MergeSortBy<T>(a: seq<T>, compare: (T, T) -> bool): (result :seq<T>)


Suggested change

function method MergeSortBy<T>(a: seq<T>, compare: (T, T) -> bool): (result :seq<T>)

function method MergeSortBy<T>(a: seq<T>, lessEqThan: (T, T) -> bool): (result :seq<T>)

It's perhaps worth noting that we could change this in the future without breaking client code. I'd maybe prefer lessEq or lessThanOrEq, to avoid the awkward reading of "equal than".

Thanks for suggestions , I am changing compare to lessThanOrEq.

@MikaelMayer I just noticed you had some style requests that were lost in the shuffle. I'll respond to the ones I see that still seem relevant, but please just provide a quick comment at the top level if there are others we missed.

Re: the naming convention for predicates, e.g. "IsTotalOrder" instead of "TotalOrder", that's potentially a good idea but the latter convention is already established here in predicates like Functions.Injective. I'd suggest if you still feel strongly about it that you cut a repo issue for discussion, similar to #47.

Re: "lessThan" instead of "less", I don't have a strong opinion so I'd be willing to change it, personally. @prvshah51?

Could you use the attribute {:options "/functionSyntax:4"} and change all your predicate method to predicate ?

function method {:opaque} Sort(s: seq, compare: (T, T) -> bool)
instead of a method

Add the following comment to MergeSortBy
// Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using MergeSortedBy

Could you use the attribute {:options "/functionSyntax:4"} and change all your predicate method to predicate ?

function method {:opaque} Sort(s: seq, compare: (T, T) -> bool)
instead of a method

I did that for MergeSort.dfy, but for Relations.dfy SortedBy was the only predicate method, and I actually made that a non-compiled predicate instead like the others. As per my comment on the original version in dafny-reportgenerator:

// TODO: Make this a predicate-by-method so it has linear runtime instead of quadratic.
// For now it's only used at runtime in tests.

This change doesn't need it to be compilable yet so I'd rather address that later.

Add the following comment to MergeSortBy
// Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using
MergeSortedBy

It's already there? :)

Trying to use {:options "/functionSyntax:4"} ran into what looks like a bug in Dafny 3.5.0 (which this repo is using) that I can't reproduce with the latest. I've reverted it for now and we can come back to that too: #55

atomb

This is a nice simplification of the original. :) Ordering continues to be a tricky topic, and I left a couple of comments related to it, though I'm not sure that any of them should hold up merging.

atomb · 2022-09-14T18:00:22Z

src/Relations.dfy

+  * Note that being trichotomous implies being irreflexive.
+  */
+  predicate Trichotomous<T(!new)>(less: (T, T) -> bool) {
+    (forall x, y :: less(x, y) || x == y || less(y, x)) &&  // at least one of the three


When I commented earlier about defining this for a comparison result data type, @cpitclaudel pointed out very rightly that my first attempt wouldn't work for comparison based on projection (e.g., looking only at the first element of a tuple), and I think this definition suffers from the same problem, using == here. That's not necessarily fatal, but it's something to be aware of.

Ah, but I notice this isn't actually used anywhere at this point. Should we remove it, given that issue?

Good point, I'd prefer to remove it too now that it's unused.

atomb · 2022-09-14T18:09:12Z

src/Collections/Arrays/BinarySearch.dfy

+  import opened Relations
+
+  method BinarySearch<T>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>)
+    requires SortedBy(a[..], (x, y) => less(x, y) || x == y)


This will have the same issue I commented on for Trichotomous, making it impossible to sort by projections. Would it be possible to make the proof go through if we required TotalOrdering instead of StrictTotalOrdering?

I attempted that at first, but I was discouraged not only by verification not immediately working, but also the fact that it makes the specification messier as well: instead of

ensures r.Some? ==> r.value < a.Length && a[r.value] == key

You would need

ensures r.Some? ==> r.value < a.Length && lessThanOrEqual(a[r.value], key) && lessThanOrEqual(key, a[r.value])

Which is just plain much harder to read and understand.

I think for that reason, it makes more sense to improve this at the same time that we add comparison functions that return CmpResult instead as per #53.

MikaelMayer

I approve but I still don't feel comfortable having a comparison function called twice in a binary search.

robin-aws · 2022-09-16T16:24:28Z

I approve but I still don't feel comfortable having a comparison function called twice in a binary search.

I definitely don't love it either. Both of these implementations are far from ideal when it comes to efficiency at runtime. I'm personally much more dissatisfied with my own MergeSort here rather than the binary search: it's using s[..1] expressions to recurse, and with the current compilation behavior that involves making a new copy, so the runtime is far worse than log-linear.

This whole repository needs more work to ensure it compiles to efficient-enough code for each supported language (see #24). In fact we're not even guaranteeing it is compilable at all for each target - it doesn't work for Java and hence the existence of https://github.com/dafny-lang/libraries-without-variance.

In general, I consider it good forwards progress to have a verified but inefficient definition of a concept here, since many users can live with the inefficiency in their context. But I'm looking forward to adding a lot of by method's in the future! :)

adding Heap Sort and Bianry Search

79ebd90

robin-aws previously requested changes Aug 11, 2022

View reviewed changes

Parva Shah added 2 commits August 16, 2022 16:13

changes as suggestions

e882171

adding dependencies

c3a51f0

prvshah51 requested a review from atomb August 16, 2022 20:16

Parva Shah added 2 commits August 16, 2022 16:32

adding 'RUN' line

09dbb38

'RUN' line

f2dbbbb

atomb reviewed Aug 16, 2022

View reviewed changes

src/Collections/Arrays/BinarySearch.dfy Outdated Show resolved Hide resolved

atomb reviewed Aug 16, 2022

View reviewed changes

prvshah51 changed the title ~~adding Heap Sort and Bianry Search~~ adding Heap Sort and Binary Search Aug 17, 2022

chnages as suggested for verification

4b596c6

prvshah51 requested a review from atomb August 17, 2022 15:17

more verification changes, with successful verfication

f5f9571

prvshah51 marked this pull request as ready for review August 17, 2022 18:54

atomb requested changes Aug 17, 2022

View reviewed changes

Parva Shah added 3 commits August 17, 2022 16:57

removing predicates and lemmas not needed,formatting.

f47c558

adding copyrights info.

1da2ba8

misc.

5de4dfd

atomb reviewed Aug 17, 2022

View reviewed changes

more changes as suggested to remove unused import and formatting.

49253b7

prvshah51 requested a review from atomb August 18, 2022 16:35

atomb previously approved these changes Aug 18, 2022

View reviewed changes

atomb requested review from cpitclaudel and MikaelMayer August 18, 2022 17:11

robin-aws and others added 10 commits September 12, 2022 14:30

Revert unneeded include/import/export changes

d768fea

removed unnecessary exports, includes from more files.

dbee08c

Merge branch 'master' of https://github.com/prvshah51/libraries

39f3b1a

# Conflicts: # src/Collections/Sequences/Seq.dfy

Remove Comparison.dfy and revert to plain relations, general cleanup

5446858

Move Relations.dfy to src (ala Functions.dfy)

8a23ea0

Add combined example, change spec on binary search so it verifies!

5cda615

Making example verification cheaper, fixing Wrappers.dfy lit test

c0a6b81

Use OutputCheck instead of *.expect files

a4311b1

The latter doesn’t work well in CI here because the /verificationLogger options cause extra, unpredictable output lines

Revert remaining unneeded edits

168e791

Newline

3a5c4b9

robin-aws self-requested a review September 13, 2022 21:36

robin-aws mentioned this pull request Sep 14, 2022

Request: lexicographical orderings #52

Open

MikaelMayer reviewed Sep 14, 2022

View reviewed changes

This was referenced Sep 14, 2022

Request: support for comparison functions that return a {less than, equal, greater than} result #53

Open

Request: QuickSort (or any other more efficient alternative to MergeSort) #54

Open

atomb previously approved these changes Sep 14, 2022

View reviewed changes

change of names.

2178946

prvshah51 dismissed atomb’s stale review via 2178946 September 14, 2022 20:04

robin-aws added 3 commits September 14, 2022 14:58

Remove unused Trichotomous predicate

ca8722a

Start to use /functionSyntax:4, don’t encourage compiling SortedBy

b1f7311

Revert adding /functionSyntax:4

f2d545e

atomb approved these changes Sep 15, 2022

View reviewed changes

MikaelMayer approved these changes Sep 16, 2022

View reviewed changes

robin-aws merged commit bfbdda8 into dafny-lang:master Sep 16, 2022

prvshah51 mentioned this pull request Nov 14, 2022

Request: binary search #42

Closed




		method BinarySearch<T>(a: array<T>, key: T,compare: (T, T) -> bool) returns (r: int)



		method BinarySearch<T>(a: array<T>, key: T,compare: (T, T) -> bool) returns (r: int)
		requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i],a[j])

		import opened Wrappers = StandardLibrary.Wrappers


		predicate Reflexive<T(!new)>(R: (T, T) -> bool) {


		module StandardLibrary.UInt {

		// TODO: Depend on types defined in dafny-lang/libraries instead

	function method MergeSortBy<T>(a: seq<T>, compare: (T, T) -> bool): (result :seq<T>)
	function method MergeSortBy<T>(a: seq<T>, lessEqThan: (T, T) -> bool): (result :seq<T>)

adding Merge Sort and Binary Search #49

adding Merge Sort and Binary Search #49

Conversation

prvshah51 commented Aug 11, 2022

robin-aws left a 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

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

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

atomb left a 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

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

atomb left a comment

Choose a reason for hiding this comment

robin-aws commented Sep 13, 2022

robin-aws commented Sep 14, 2022

prvshah51 commented Sep 14, 2022 • edited Loading

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

Choose a reason for hiding this comment

atomb left a 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

robin-aws commented Sep 16, 2022

prvshah51 commented Sep 14, 2022 •

edited

Loading