kouzdra

Category:

Вторая часть мерлезонского балета: 

module Fact

use import mach.int.Int32

let rec fact (n : int32) : int32
    variant { to_int n }
    requires { to_int n >= 0 }
    ensures { to_int result >= 1 }
=
    if n = of_int 0  then of_int 1 else n * fact (n - of_int 1)

let test () = fact (of_int 50)

end
Собственно тут все думаю понятно - вместо "безразмерного" int используется int32 из пакета mach.int.Int32 (mach тут для "машинный"). of_int/to_int - просто функции явного преобразования типов.

При попытке откомпилировать оно ругается на функцию.
Замечу что если ensures убрать - все равно будет ругаться, потому что в пакете int32 переполнение считается ошибкой.

Способов пофиксить несколько - простейший - переопределить операцию * так, чтобы она выкидывала исключение при переполнении:
module Fact

use import mach.int.Int64 as I64
use import mach.int.Int32 as I32

exception Invalid_arg

let ( *) (a : int32) (b : int32) : int32
   raises { Invalid_arg }
   ensures { to_int a * to_int b = to_int result }
=
    let res = I64.(*) (I64.of_int (I32.to_int a)) (I64.of_int (I32.to_int b)) in
    if I64.(<=) res (I64.of_int max_int32) && I64.(>=) res (I64.of_int min_int32)
    then I32.of_int (I64.to_int res)
    else raise Invalid_arg

let rec fact (n : int32) : int32
    variant { to_int n }
    requires { 0 <= to_int n }
    ensures { to_int result >= 1 }
    raises { Invalid_arg }
=
    if n = of_int 0 then of_int 1 else fact (n - of_int 1) * n

let test () raises { Invalid_arg } = fact (I32.of_int 50)

end

В комментариях тут пожалуй нуждается только ensures { to_int a * to_int b = to_int result } в определении операции *:

у WhyML подход тут довольно простой - он сам не пытается проявлять интеллект в контракты функций - потому тут надо сказать что * - это действительно умножение.

В случае с факториалом есть и более хитрый (но и более вообще говоря удобный при ее использовании) подход - но это уже сильно потом.

PS: Специально для Гастрита отмечу что сделать модуль IntMod32 не только можно - но и очень просто - часика два максимум писанины - просто описать аксиоматику соответствующего поля и все - просто наследуешься от algebra.OrderedCommutativeRing и описываешь свойства операций в этом поле.

LJ Video