mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
45 lines
596 B
Plaintext
45 lines
596 B
Plaintext
|
|
|
|
module ArrayUpdate
|
|
|
|
use int.Int
|
|
use array.Array
|
|
|
|
let test (a:array int)
|
|
requires { a.length >= 1 }
|
|
=
|
|
label L in
|
|
a[0] <- 42;
|
|
assert { a = (a at L)[0 <- 42] }
|
|
|
|
|
|
end
|
|
|
|
|
|
module ImpMapUpdate
|
|
|
|
clone impmap.ImpmapNoDom with type key = int
|
|
|
|
let test (m:t int) =
|
|
label L in
|
|
m[0] <- 42;
|
|
assert { m = (m at L)[0 <- 42] }
|
|
|
|
|
|
|
|
end
|
|
|
|
module ArrayFunctionalUpdate
|
|
|
|
use int.Int
|
|
use array.Array
|
|
|
|
predicate p (array int)
|
|
|
|
let test (a:array int) (i:int)
|
|
requires { 0 <= i < a.length }
|
|
requires { p (a[i<-42]) }
|
|
= a[i] <- 42;
|
|
assert { p a }
|
|
|
|
end |