mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
35 lines
446 B
Plaintext
35 lines
446 B
Plaintext
|
|
module A
|
|
|
|
use int.Int
|
|
use array.Array
|
|
|
|
let f1 (a:array int) : int
|
|
= a[0]
|
|
|
|
let f2 (a:array int) : unit
|
|
requires { a.length >= 2 }
|
|
ensures { a[0] <> a[1] }
|
|
= a[0] <- 42
|
|
|
|
end
|
|
|
|
module B
|
|
|
|
use int.Int
|
|
use array.Array
|
|
clone array.Sorted with
|
|
type elt=int,
|
|
predicate le=(<=)
|
|
|
|
|
|
let f1 (a:array int) : unit
|
|
ensures { sorted a }
|
|
= ()
|
|
|
|
|
|
let f2 (a:array int) : array int
|
|
ensures { sorted result }
|
|
= a
|
|
|
|
end |