mirror of
https://github.com/kmc7468/cs220.git
synced 2025-12-12 21:08:45 +00:00
45 lines
1.4 KiB
Plaintext
45 lines
1.4 KiB
Plaintext
(* Pascal
|
|
|
|
Prove that the Pascal's triangle indeed computes combinations.
|
|
HINT: https://en.wikipedia.org/wiki/Pascal%27s_triangle
|
|
*)
|
|
|
|
module Pascal
|
|
|
|
use int.Int
|
|
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)
|
|
|
|
(* Computes 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 Pascal's triangle first to find good invariants. *)
|
|
let chooses (n : int) : array int
|
|
requires { n > 0 }
|
|
ensures { forall i: int.
|
|
0 <= i < length result -> result[i] = comb n i }
|
|
=
|
|
let ref row = Array.make 1 1 in
|
|
for r = 1 to n do
|
|
invariant { length row = r }
|
|
invariant { forall c: int. 0 <= c < r -> row[c] = comb (r-1) c }
|
|
let new_row = Array.make (r+1) 1 in
|
|
for c = 1 to r-1 do
|
|
(* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
|
|
(* TODO: Replace `true` with your solution. Your solution MUST be a single line, at line 36. DON'T add more code above or below. *)
|
|
invariant { true }
|
|
(* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
|
|
new_row[c] <- row[c-1] + row[c]
|
|
done;
|
|
row <- new_row
|
|
done;
|
|
row
|
|
|
|
end
|