## Two puzzles from Danvy and Goldberg's ``There and back again''

Authors: Jean-Christophe Filliâtre

Topics: List Data Structure

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(* Two puzzles from Danvy and Goldberg's ``There and back again''
http://www.brics.dk/RS/02/12/BRICS-RS-02-12.pdf‎
*)

(* Computing a symbolic convolution:
Given two lists [x1 , x2 , ..., xn−1 , xn ] and
[y1 , y2 , ..., yn−1 , yn ], where n is not known in advance,
write a function that constructs
[(x1 , yn ), (x2 , yn−1 ), ..., (xn−1 , y2 ), (xn , y1 )]
in n recursive calls and with no auxiliary list.
*)

module Convolution

use int.Int
use list.List
use list.Length
use list.Append
use list.Reverse
use list.Combine

let rec convolution_rec (x y: list 'a) : (list ('a, 'a), list 'a)
variant  { x }
requires { length x <= length y }
ensures  { let r, ys = result in exists y0: list 'a.
y = y0 ++ ys && length y0 = length x &&
r = combine x (reverse y0) }
= match x with
| Nil ->
Nil, y
| Cons x0 xs ->
match convolution_rec xs y with
| r, Cons y0 ys -> Cons (x0, y0) r, ys
| _ -> absurd end
end

let convolution (x y: list 'a) : list ('a, 'a)
requires { length x = length y }
ensures  { result = combine x (reverse y) }
= let r, _ = convolution_rec x y in r

end

(* Detecting a palindrome:
Given a list of length n, where n is not known in advance,
determine whether this list is a palindrome in ceil(n/2) recursive
calls and with no auxiliary list.
*)

module Palindrome

use int.Int
use option.Option
use list.List
use list.Length
use list.Append
use list.Nth
use list.NthLength
use list.NthLengthAppend

predicate pal (x: list 'a) (n: int) =
forall i: int. 0 <= i < n -> nth i x = nth (n - 1 - i) x

exception Exit

type elt
val predicate eq (x y: elt)
ensures { result <-> x = y }

let rec palindrome_rec (x y: list elt): list elt
requires { length x >= length y }
variant { x }
ensures { exists x0: list elt. length x0 = length y && x = x0 ++ result }
ensures { pal x (length y) }
raises  { Exit -> exists i: int. 0 <= i < length y &&
nth i x <> nth (length y - 1 - i) x }
= match x, y with
| _, Nil ->
x
| Cons _  xs, Cons _ Nil ->
xs
| Cons x0 xs, Cons _ (Cons _ ys) ->
match palindrome_rec xs ys with
| Cons x1 xs ->
assert { nth (length y - 1) x = Some x1 };
if eq x0 x1 then xs else raise Exit
| Nil -> absurd
end
| _ -> absurd
end

let palindrome (x: list elt) : bool
ensures { result=True <-> pal x (length x) }
= match palindrome_rec x x with _ -> True
| exception Exit -> False end

end
```