Commit b4711106 authored by MARCHE Claude's avatar MARCHE Claude

implementation of bigInts in Why3

parent 74f28874
(** A library for arbitrary-precision integer arithmetic *)
module N
use import mach.int.Int31
use import mach.array.Array31
use import ref.Ref
use import int.Int
constant base : int = 32768
type t = { mutable digits: array int31 }
predicate ok_array (a:array int31) =
forall i:int. 0 <= i < to_int a.length ->
0 <= to_int a[i] < base
predicate ok (x:t) = ok_array x.digits
function value_from (x:array int31) (n:int) : int
axiom value_from_next:
forall x,n. 0 <= n < to_int x.length ->
value_from x n = to_int x[n] + base * value_from x (n+1)
axiom value_from_end:
forall x,n. n = to_int x.length ->
value_from x n = 0
function value_array (x:array int31) : int = value_from x 0
function value (x:t) : int = value_array x.digits
let from_small_int (n:int31) : t
requires { 0 <= to_int n < base }
ensures { ok result }
ensures { value result = to_int n }
=
let a = Array31.make (of_int 1) n in
{ digits = a }
exception TooManyDigits
let add_array (x y:array int31) : array int31
requires { ok_array x /\ ok_array y }
requires { to_int x.length <= to_int y.length }
ensures { ok_array result }
ensures { value_array result = value_array x + value_array y }
raises { TooManyDigits -> true }
=
let zero = of_int 0 in
let one = of_int 1 in
let base31 = of_int base in
let l = x.length in
let h = y.length in
if Int31.(>=) h (of_int Int31.max_int31) then raise TooManyDigits;
let arr = Array31.make (Int31.(+) h one) zero in
let carry = ref zero in
let i = ref zero in
while Int31.(<) !i l do
invariant { 0 <= to_int !i <= to_int l }
invariant { 0 <= to_int !carry <= 1 }
invariant { forall j. 0 <= j < to_int !i ->
0 <= to_int arr[j] < base }
variant { to_int l - to_int !i }
let sum = Int31.(+) (Int31.(+) x[!i] y[!i]) !carry in
if Int31.(>=) sum base31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
else begin arr[!i] <- sum; carry := zero end;
i := Int31.(+) !i one;
done;
while Int31.(<) !i h do
invariant { 0 <= to_int !i <= to_int h }
invariant { 0 <= to_int !carry <= 1 }
invariant { forall j. 0 <= j < to_int !i ->
0 <= to_int arr[j] < base }
variant { to_int h - to_int !i }
let sum = Int31.(+) y[!i] !carry in
if Int31.(>=) sum base31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
else begin arr[!i] <- sum; carry := zero end;
i := Int31.(+) !i one;
done;
arr[!i] <- !carry;
arr
let add (x y:t) : t
requires { ok x /\ ok y }
ensures { ok result }
ensures { value result = value x + value y }
raises { TooManyDigits -> true }
= let l1 = x.digits.length in
let l2 = y.digits.length in
let res =
if Int31.(<=) l1 l2 then
add_array x.digits y.digits
else add_array y.digits x.digits
in
{ digits = res }
end
\ No newline at end of file
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment