vstd/
math.rs

Help
1#[allow(unused_imports)]
2use super::prelude::*;
3
4verus! {
5
6/// This function computes the minimum of two given integers.
7pub open spec fn min(x: int, y: int) -> int {
8    if x <= y {
9        x
10    } else {
11        y
12    }
13}
14
15/// This function computes the maximum of two given integers.
16pub open spec fn max(x: int, y: int) -> int {
17    if x >= y {
18        x
19    } else {
20        y
21    }
22}
23
24/// This function computes the maximum of three given integers.
25pub open spec fn max3(x: int, y: int, z: int) -> int {
26    if x < y {
27        max(y, z)
28    } else {
29        max(x, z)
30    }
31}
32
33/// This function converts the given integer `x` to a natural number
34/// by returning 0 when `x` is negative and `x` otherwise.
35pub open spec fn clip(x: int) -> nat {
36    if x < 0 {
37        0
38    } else {
39        x as nat
40    }
41}
42
43/// This function computes the absolute value of a given integer.
44pub open spec fn abs(x: int) -> nat {
45    if x < 0 {
46        -x as nat
47    } else {
48        x as nat
49    }
50}
51
52/// This function adds two integers together. It's sometimes
53/// useful as a substitute for `+` in triggers that feature
54/// function invocations, since mathematical operators can't be
55/// mixed with function invocations in triggers.
56pub open spec fn add(x: int, y: int) -> int {
57    x + y
58}
59
60/// This function subtracts two integers. It's sometimes useful as
61/// a substitute for `-` in triggers that feature function
62/// invocations, since mathematical operators can't be mixed with
63/// function invocations in triggers.
64pub open spec fn sub(x: int, y: int) -> int {
65    x - y
66}
67
68/// This function divides two integers. It's sometimes useful as a
69/// substitute for `/` in triggers that feature function
70/// invocations, since mathematical operators can't be mixed with
71/// function invocations in triggers.
72pub open spec fn div(x: int, y: int) -> int {
73    x / y
74}
75
76} // verus!
vstd/math.rs

vstd/
math.rs
