diff --git a/dafny/2021/dafny_exercises_2021.pdf b/dafny/2021/dafny_exercises_2021.pdf index d21d69e..eac6970 100644 Binary files a/dafny/2021/dafny_exercises_2021.pdf and b/dafny/2021/dafny_exercises_2021.pdf differ diff --git a/dafny/2021/tasks_2021.dfy b/dafny/2021/tasks_2021.dfy index c13833b..d4e14c8 100644 --- a/dafny/2021/tasks_2021.dfy +++ b/dafny/2021/tasks_2021.dfy @@ -123,26 +123,6 @@ method bubble_sort3(A:array) } } -// Task 6. Difficulty: * -function method get_min(a:int, b:int) : int -{ - if a <= b then a else b -} - -method sort3(a:int, b:int, c:int) returns (min:int, mid:int, max:int) -ensures min in {a,b,c} -ensures mid in {a,b,c} -ensures max in {a,b,c} -ensures a in {min, mid, max} -ensures b in {min, mid, max} -ensures c in {min, mid, max} -ensures min <= mid <= max -{ - min := get_min(a, get_min(b,c)); - max := -get_min(-a, get_min(-b,-c)); - mid := a + b + c - max - min; -} - method print_array(A:array) { var i := 0;