blob: 32b302f3404f1117c25f5b854625d50fd6eb17ec (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
type{:datatype} finite_map;
function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;
type{:datatype} partition;
function{:constructor} partition(owners:[int]int, vars:[int]finite_map):partition;
procedure P(arr:finite_map)
requires dom#finite_map(arr)[0];
ensures dom#finite_map(arr)[0];
{
}
|
