Language snippet

snippet thingy

proc write(key: str, value: T) modifies store {
  store[key] := value;
}

fun read(key: str) returns (out:T)  {
  out := store[key];
}

// ....

properties A
gen {
  , store: empty()
  , keys: gen(str) { props }
  , vals: get(T) {}
}
{
  prop "adding a diff key doesn't modify the old key" {
     // ...
  }
  
  prop "writes are retrievable" {
    // ...
  }
  
  prop "fuzz" {
    // ...
  }
}