kmc7468/cs220
1
0
Fork 0
mirror of https://github.com/kmc7468/cs220.git synced 2025-12-12 21:08:45 +00:00
Code Issues Packages Projects Releases Wiki Activity

why3 assignment: add one-line comment, fixed max spec

Browse Source
This commit is contained in:
AnHaechan
2023-08-29 07:29:56 +00:00
committed by Jeehoon Kang
parent be4fc57edb
commit e5b80e7365
2 changed files with 24 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
assets/why3/assignment05/max.mlw
View File

@@ -1,9 +1,14 @@
(* Max
Given an array `a` of natural numbers with length `n`,
return the maximum element of the array.
Given an array `a` of integers with length `n` greater than `0`,
return `max_idx`, the index of the maximum element of that array.
You should stengthen the loop invariant.
E.g. `max_idx [5, 12, 34, 10] 4` will return `2`
E.g. `max_idx [4, 3, 2] 3` will return `0`
E.g. `max_idx [1, 2, 3, 4] 4` will return `3`
Prove the below program indeed follows the given specification,
by giving an appropriate invariant.
*)
module Max
@@ -12,18 +17,21 @@ module Max
use ref.Ref
use array.Array
let max (a: array int) (n: int) : (max: int)
let max_idx (a: array int) (n: int) : (max_idx: int)
requires { length a > 0 }
requires { n = length a }
requires { forall i. 0 <= i < n -> a[i] >= 0 }
ensures { forall i. 0 <= i < n -> a[i] <= max }
ensures { exists i. 0 <= i < n -> a[i] = max }
= let ref max = 0 in
ensures { 0 <= max_idx <= n-1 }
ensures { forall i. 0 <= i <= n-1 -> a[i] <= a[max_idx] }
=
let ref max_idx = 0 in
for i = 0 to n-1 do
invariant { 0 <= max_idx <= n-1 }
(* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
invariant { true (* TODO: Replace `true` with your solution *) }
invariant { true (* TODO: Replace `true` with your solution. Your solution MUST be a single line, at line number 30. DON'T add another line of codes. *) }
(* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
if max < a[i] then max <- a[i];
if a[max_idx] < a[i] then max_idx <- i;
done;
max
max_idx
end

6
assets/why3/assignment05/pascal.mlw
View File

@@ -10,13 +10,15 @@ module Pascal
use ref.Ref
use array.Array
(* The mathematical combination, defined recursively. *)
let rec function comb (n k: int) : int
requires { 0 <= k <= n }
variant { n }
ensures { result >= 1 }
= if k = 0 || k = n then 1 else comb (n-1) k + comb (n-1) (k-1)
(* Insert appropriate invariants so that Why3 can verify this function. *)
(* Computes the Pascal's triangle and returns the `n`th row of it. *)
(* Insert an appropriate invariant so that Why3 can verify this function. *)
(* You SHOULD understand the Pascal's triangle first to find good invariants. *)
let chooses (n : int) : array int
requires { n > 0 }
@@ -30,7 +32,7 @@ module Pascal
let new_row = Array.make (r+1) 1 in
for c = 1 to r-1 do
(* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
invariant { true (* TODO: Replace `true` with your solution *) }
invariant { true (* TODO: Replace `true` with your solution. Your solution MUST be a single line, at line number 35. DON'T add another lines. *) }
(* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
new_row[c] <- row[c-1] + row[c]
done;