mozilla/rust — Issue #1809: Mutable values in predicate arguments break typestate checks
Author: vlasovskikh
Created: 2012-02-10 22:37:49+00:00
State: open

Consider the following example in Rust 0.1:

use std;

type s = {mutable x: int};

pure fn is_non_negative(&s: s) -> bool { s.x >= 0 } // should not compile, violates referential transparency

fn get_non_negative_x(s: s): is_non_negative(s) -> int { s.x }

#[test]
fn test1() {
let s = {mutable x: 0};
check is_non_negative(s);
s.x = -1;
let x = get_non_negative_x(s);
assert x >= 0; // should pass, but fails
}

The predicate `pure fn is_non_negative(&s: s) -> bool` should guarantee, that the field `s.x` is not negative, so `fn get_non_negative(s: s) -> int` should return a value greater or equal to `0`. But due to mutability of `s.x` this may be not true. And it does in the example above, so the `assert x >= 0` fails.