anthem-rs/examples/example-2.spec

# Perform the proofs under the assumption that n is a nonnegative integer input constant
input: n -> integer.
assume: n >= 0.

# p/1 is an auxiliary predicate
output: q/1.

# Verify that q computes the floor of the square root of n
spec: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
Add comments to example 2 2020-05-12 06:10:59 +02:00			`# Perform the proofs under the assumption that n is a nonnegative integer input constant`
Improve output 2020-05-07 17:19:42 +02:00			`input: n -> integer.`
Add comments to example 2 2020-05-12 06:10:59 +02:00			`assume: n >= 0.`

Simplify examples 2020-05-28 07:06:19 +02:00			`# p/1 is an auxiliary predicate`
Add parser support for output statements 2020-05-12 05:27:51 +02:00			`output: q/1.`
Add examples 2020-05-06 21:39:04 +02:00
Simplify examples 2020-05-28 07:06:19 +02:00			`# Verify that q computes the floor of the square root of n`
Rename “assert” statement to “spec” 2020-05-22 18:34:59 +02:00			`spec: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).`