supleed2/ELEC70056-HSV-CW1
1
0
Fork 0
mirror of https://github.com/supleed2/ELEC70056-HSV-CW1.git synced 2024-09-19 20:46:16 +00:00
Code Issues Packages Projects Releases Wiki Activity

removed task 6

Browse source
This commit is contained in:
John Wickerson 2021-11-01 10:03:55 +00:00
parent 0e8514ef99
commit cbe8f0fb9c
2 changed files with 0 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
dafny/2021/dafny_exercises_2021.pdf
View file

Binary file not shown.

20
dafny/2021/tasks_2021.dfy
View file

@ -123,26 +123,6 @@ method bubble_sort3(A:array<int>)
}
}
// 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<int>)
{
var i := 0;