diceprop

随机测试的数学属性集合。

它基于 dicetest.

此 Crates 的状态

作者认为这个 Crates 还不稳定。变更将在 变更日志 中记录。

示例

结合二进制操作

use diceprop::{props, Fun2, Set};
use dicetest::prelude::*;

#[test]
fn add_is_associative_for_small_f32() {
    Dicetest::repeatedly().run(|mut fate| {
        let set = Set::new("f32 ∩ [-100,100]", dice::f32(-100.0..=100.0));
        let vars = fate.roll(set.vars(["x", "y", "z"]));
        let add = Fun2::infix("+", |x, y| x + y);
        props::binop::associative(vars, add);
    })
}

测试失败，以下为输出

The test failed after 12 passes.

# Config
- seed: 14859458141222391139
- start limit: 0
- end limit: 100
- passes: 200

# Counterexample
- run code: "2pYRCj9fj8sV52fB5iyFhxCISGY3nKlMzlzIKq0NKLwGAAAAAAAAAA=="
- limit: 6
- hints:
        - Is `+` associative?
                - x, y, z of f32 ∩ [-100,100]
                - x = 96.621735
                - y = -90.97134
                - z = -8.10239
                - (x + y) = 5.6503983
                - ((x + y) + z) = -2.451992
                - (y + z) = -99.07373
                - (x + (y + z)) = -2.4519958
                - (((x + y) + z) == (x + (y + z))) = false
- error: assertion failed: (((x + y) + z) == (x + (y + z)))

左逆函数

use diceprop::{props, Fun1, Set};
use dicetest::prelude::*;

#[test]
fn sqrt_is_left_inverse_of_sq_for_non_negative_f32() {
    Dicetest::repeatedly().run(|mut fate| {
        let set = Set::new("f32 ∩ [0,+∞]", dice::f32(0.0..));
        let vars = fate.roll(set.vars(["x"]));
        let sq = Fun1::postfix("²", |x| x * x);
        let sqrt = Fun1::new("√", |x: f32| x.sqrt());
        props::fun::left_inverse(vars, sq, sqrt);
    })
}

测试失败，以下为输出

The test failed after 0 passes.

# Config
- seed: 7632522237817347676
- start limit: 0
- end limit: 100
- passes: 200

# Counterexample
- run code: "F2/nnlbX6qyCOm5MU7P8BSXdnJ4XNXJdihgwhtWxlzMAAAAAAAAAAA=="
- limit: 0
- hints:
        - Is `√` left inverse of `²`?
                - x of f32 ∩ [0,+∞]
                - x = 305770290000000000000000000000000000000.0
                - (x)² = inf
                - √((x)²) = inf
                - (√((x)²) == x) = false
- error: assertion failed: (√((x)²) == x)

偏序

use diceprop::{props, Fun2, Set};
use dicetest::prelude::*;

#[test]
fn gt_is_partial_order_for_any_f32() {
    Dicetest::repeatedly().run(|mut fate| {
        let set = Set::new("f32", dice::any_f32());
        let vars = fate.roll(set.vars(["x", "y", "z"]));
        let gt = Fun2::infix("≤", |x, y| x <= y);
        props::binrel::partial_order(vars, gt);
    })
}

测试失败，以下为输出

The test failed after 3 passes.

# Config
- seed: 18374838706510982620
- start limit: 0
- end limit: 100
- passes: 200

# Counterexample
- run code: "h6jQMNr6fi/j9OZOXmklXYAUATM96EpE6+DENMhSZHkBAAAAAAAAAA=="
- limit: 1
- hints:
        - Is `≤` a partial order?
                - Is `≤` reflexive?
                        - x of f32
                        - x = NaN
                        - (x ≤ x) = false
- error: assertion failed: (x ≤ x)

许可证

根据您的选择，许可协议为

• Apache 许可协议第 2 版 (LICENSE-APACHE 或 http://www.apache.org/licenses/LICENSE-2.0)
• MIT 许可协议 (LICENSE-MIT 或 http://opensource.org/licenses/MIT)

。

贡献

除非您明确说明，否则根据 Apache-2.0 许可协议定义，您有意提交以包含在工作中的任何贡献都应按上述方式双重许可，不附加任何其他条款或条件。