kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

Продолжаю разираться с Why3

Очень поучительно (кроме практической пользы) в плане менее навороченной и в некотором смысле "промежуточной" альтернативы всякой науке про зависимые и рафинированные типы и прочее - примерно как Ocaml полезен в качестве "промежуточной" к Haskell ступеньки (еще и куда более практичной, тоже).

Щас осознал откуда берется естественным образом идея необязательных (в смысле автоматически определяемых из контекста) параметров:

И правда:
let reverse (n : int) (src : array 'a) (dst : array 'a) 
   requires { src.length = n = dst.length }
   ensures  { forall i : int . (0 <= i < n -> dst [n - 1 - i] = src [i]) }
	=
   for i =  0 to n - 1 do
	invariant { forall k : int . (0 <= k < i -> dst [n - 1 - k] = src [k]) } 
	dst [n - 1 - i] <- src [i] 
   done
Выглядит в некотором роде "симметричнее" и "естественнее" чем
let reverse (src : array 'a) (dst : array 'a) 
   requires { src.length = dst.length }
   ensures  { forall i : int . (0 <= i < src.length -> dst [src.length - 1 - i] = src [i]) }
...
Но писать явно параметр n как-то лишнее - поскольку он легко и однозначно определяется из контекста - потому возникает естественно желание ввести (отсутствующую в Why3, потому как WhyML предназначен не для программирования, а скорее как промежуточный язык) конструкцию вроде:
let reverse {n : int} (src : array 'a) (dst : array 'a) 
   requires { src.length = n = dst.length }
...
Которую так любят в всяких agda'х и F*-х. Там впрочем она является почти необходимостью* потому как на зависимых типах вариант без параметра n написать не получается - типам массива надо от чего-то зависеть

PS: В качестве просто приятного примера-а - тест:
...
    let a = ... in
    let b = make n 0 in
    let c = make n 0 in
    reverse n a b;
    reverse n b c;
    assert { forall i : int . (0 <= i < n -> a [i] = c [i]) };
    ...

Что приятно - assert, утверждающий что два переворачивания вектора оставляют все на месте вполне успешно доказывается (в WhyML ассерты, которые не удалось доказать считаются ошибкой при чекинге, для недоказуемых с динамической проверкой существует оператор check, для недоказуемых без проверки - assume)

*) Кстати необходимость загромождать код пусть и неявными, но довольно многочисленными по факту параметрами не очень красит идею с зависимыми типами - тоже полезное осознание от опытов
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 6 comments