Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[DMS-60] enhance todo showcase #36

Merged
merged 2 commits into from
Jul 1, 2024
Merged

[DMS-60] enhance todo showcase #36

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4a9668c
[motoko-san] enhance todo showcase
GoPavel Jun 30, 2024
ca7663a
[motoko-san] rename field in todo_record.mo showcase
GoPavel Jun 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
106 changes: 68 additions & 38 deletions test/viper/ok/todo_record.vpr.ok
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(
define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
/* Tuple encoding */
adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
/* Option encoding */
adt Option[T] {
None()
Expand All @@ -27,7 +28,7 @@ define $Perm($Self) ((((true && (acc(($Self).todos,write) && $array_acc(
($Self).todos,
$c_ToDo, write))) &&
acc(($Self).num,write)) && acc(($Self).nextId,write)))
define $Inv($Self) (invariant_14($Self))
define $Inv($Self) ((invariant_14($Self) && invariant_15($Self)))
method __init__($Self: Ref)

requires $Perm($Self)
Expand All @@ -41,21 +42,27 @@ method __init__($Self: Ref)
($Self).nextId := 1;
}
adt ToDo
{ $RecordCtor_ToDo($ToDo$completed : State, $ToDo$desc : Int,
$ToDo$id : Int) }
{ $RecordCtor_ToDo($ToDo$desc : Int, $ToDo$id : Int, $ToDo$state : State) }
adt State { DONE()
TODO() }
field todos: Array
field num: Int
field nextId: Int
define invariant_14($Self) (((0 <= ($Self).num) && (($Self).num <= $size(
($Self).todos))))
define invariant_15($Self) ((forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id <
($Self).nextId))))
method resize($Self: Ref, n: Int)

requires $Perm($Self)
requires ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
requires (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId)))
ensures $Perm($Self)
ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId)))
ensures ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
ensures ($size(($Self).todos) >= n)
Expand All @@ -71,12 +78,14 @@ method resize($Self: Ref, n: Int)
assert (n >= 0);
inhale $array_acc(new_array, $c_ToDo, write);
inhale ($size(new_array) == n);
inhale $array_init(new_array, $c_ToDo, $RecordCtor_ToDo(TODO(), 0, 0));
inhale $array_init(new_array, $c_ToDo, $RecordCtor_ToDo(0, 0, TODO()));
i := 0;
while ((i < $size(($Self).todos)))
invariant $Perm($Self)
invariant $array_acc(new_array, $c_ToDo, write)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ((0 <= i) && (i <= $size(($Self).todos)))
Expand Down Expand Up @@ -110,15 +119,15 @@ method getTodos($Self: Ref)
{ var new_array: Array
inhale $array_acc(new_array, $c_ToDo, write);
inhale ($size(new_array) == 1);
($loc(new_array, 0)).$c_ToDo := $RecordCtor_ToDo(TODO(), 0, 0);
($loc(new_array, 0)).$c_ToDo := $RecordCtor_ToDo(0, 0, TODO());
exhale $array_acc(new_array, $c_ToDo, wildcard);
inhale $array_acc(new_array, $c_ToDo, wildcard);
$Res := new_array;
goto $Ret;
label $Ret;
}
method getTodo($Self: Ref, id: Int)
returns ($Res: Option[ToDo])
returns ($Res: Tuple$2[Option[ToDo], Int])
requires $Perm($Self)
requires $Inv($Self)
ensures $Perm($Self)
Expand All @@ -131,7 +140,18 @@ method getTodo($Self: Ref, id: Int)
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==>
(exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(($loc(
($Self).todos,
i)).$c_ToDo) == $Res))))
i)).$c_ToDo) ==
($Res).tup$2$0))))
ensures ((($Res).tup$2$0 == None()) == (forall i : Int :: (((0 <= i) && (i <
($Self).num)) ==> ((($loc(
($Self).todos,
i)).$c_ToDo).$ToDo$id != id))))
ensures ((($Res).tup$2$0 != None()) ==> ((0 <= ($Res).tup$2$1) && (
($Res).tup$2$1 < $size(($Self).todos))))
ensures ((($Res).tup$2$0 != None()) ==> (($Res).tup$2$0 == Some((
$loc(
($Self).todos,
($Res).tup$2$1)).$c_ToDo)))
ensures $Inv($Self)
{ var i: Int
var res: Option[ToDo]
Expand All @@ -140,6 +160,8 @@ method getTodo($Self: Ref, id: Int)
while ((i < ($Self).num))
invariant $Perm($Self)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ($size(($Self).todos) == old($size(($Self).todos)))
Expand All @@ -148,6 +170,13 @@ method getTodo($Self: Ref, id: Int)
($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos,
ii)).$c_ToDo))))
invariant ((0 <= i) && (i <= ($Self).num))
invariant ((forall j : Int :: (((0 <= j) && (j < i)) ==> ((
(
$loc(
($Self).todos,
j)).$c_ToDo).$ToDo$id != id))) == (res ==
None()))
invariant ((res != None()) ==> (res == Some(($loc(($Self).todos, i)).$c_ToDo)))
{
label $lbl$continue$l;
if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))
Expand All @@ -157,7 +186,7 @@ method getTodo($Self: Ref, id: Int)
};
};
label $lbl$l;
$Res := res;
$Res := Tup$2(res, i);
goto $Ret;
label $Ret;
}
Expand All @@ -170,11 +199,10 @@ method addTodo($Self: Ref, description: Int)
ensures (($Self).num == (old(($Self).num) + 1))
ensures (($Self).nextId == (old(($Self).nextId) + 1))
ensures ($Res == old(($Self).nextId))
ensures (($loc(($Self).todos, (($Self).num - 1))).$c_ToDo == $RecordCtor_ToDo(
TODO(),
description,
$Res))
ensures (forall i : Int :: (((0 <= i) && ((i + 1) < ($Self).num)) ==> (
ensures (($loc(($Self).todos, (($Self).num - 1))).$c_ToDo == $RecordCtor_ToDo(description,
$Res,
TODO()))
ensures (forall i : Int :: (((0 <= i) && (i < (($Self).num - 1))) ==> (
($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))
ensures $Inv($Self)
{ var id: Int
Expand All @@ -183,8 +211,8 @@ method addTodo($Self: Ref, description: Int)
{
resize($Self, ((($Self).num * 2) + 1));
};
($loc(($Self).todos, ($Self).num)).$c_ToDo := $RecordCtor_ToDo(
TODO(), description, id);
($loc(($Self).todos, ($Self).num)).$c_ToDo := $RecordCtor_ToDo(description,
id, TODO());
($Self).num := (($Self).num + 1);
($Self).nextId := (($Self).nextId + 1);
$Res := id;
Expand All @@ -204,13 +232,15 @@ method completeTodo($Self: Ref, id: Int)
($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))
ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == DONE())))
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == DONE())))
ensures $Inv($Self)
{ var i: Int
i := 0;
while ((i < ($Self).num))
invariant $Perm($Self)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((0 <= i) && (i <= $size(($Self).todos)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
Expand All @@ -224,21 +254,20 @@ method completeTodo($Self: Ref, id: Int)
ii)).$c_ToDo))))
invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id == id)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$completed ==
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$state ==
DONE())))
{
if (true)
{ var taskId: Int
var taskDesc: Int
var _completed: State
var _state: State
taskId := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id;
taskDesc := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$desc;
_completed := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed;
_state := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$state;
if ((taskId == id))
{
($loc(($Self).todos, i)).$c_ToDo := $RecordCtor_ToDo(
DONE(), taskDesc,
taskId);
($loc(($Self).todos, i)).$c_ToDo := $RecordCtor_ToDo(taskDesc,
taskId, DONE());
};
i := (i + 1);
};
Expand All @@ -263,6 +292,8 @@ method showTodos($Self: Ref)
while ((i < ($Self).num))
invariant $Perm($Self)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ($size(($Self).todos) == old($size(($Self).todos)))
Expand All @@ -272,12 +303,12 @@ method showTodos($Self: Ref)
{ var todo: ToDo
todo := ($loc(($Self).todos, i)).$c_ToDo;
output := $concat($concat(output, 2), (todo).$ToDo$desc);
if (((todo).$ToDo$completed).isDONE)
if (((todo).$ToDo$state).isDONE)
{
output := $concat(output, 3);
}else
{
if (((todo).$ToDo$completed).isTODO)
if (((todo).$ToDo$state).isTODO)
{
output := $concat(output, 4);
};
Expand All @@ -287,7 +318,7 @@ method showTodos($Self: Ref)
goto $Ret;
label $Ret;
}
method clearCompleted($Self: Ref)
method clearstate($Self: Ref)

requires $Perm($Self)
requires $Inv($Self)
Expand All @@ -296,28 +327,27 @@ method clearCompleted($Self: Ref)
ensures (($Self).nextId == old(($Self).nextId))
ensures ($size(($Self).todos) == old($size(($Self).todos)))
ensures (forall i : Int :: ((((0 <= i) && (i < old(($Self).num))) && (
old((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed) ==
TODO())) ==> (exists k : Int :: (((0 <= k) && (k < $size(
($Self).todos))) && (
($loc(($Self).todos, k)).$c_ToDo == old(($loc(
($Self).todos,
i)).$c_ToDo))))))
old((($loc(($Self).todos, i)).$c_ToDo).$ToDo$state) == TODO())) ==>
(exists k : Int :: (((0 <= k) && (k < $size(($Self).todos))) && (
($loc(($Self).todos, k)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))))
ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == TODO())))
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == TODO())))
ensures $Inv($Self)
{ var new_array: Array
var i: Int
var j: Int
assert ($size(($Self).todos) >= 0);
inhale $array_acc(new_array, $c_ToDo, write);
inhale ($size(new_array) == $size(($Self).todos));
inhale $array_init(new_array, $c_ToDo, $RecordCtor_ToDo(TODO(), 0, 0));
inhale $array_init(new_array, $c_ToDo, $RecordCtor_ToDo(0, 0, TODO()));
i := 0;
j := 0;
while ((i < ($Self).num))
invariant $Perm($Self)
invariant $array_acc(new_array, $c_ToDo, write)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ($size(($Self).todos) == old($size(($Self).todos)))
Expand All @@ -330,17 +360,17 @@ method clearCompleted($Self: Ref)
invariant (j <= i)
invariant ((0 <= j) && (j <= ($Self).num))
invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$completed ==
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$state ==
TODO())) ==> (exists k : Int :: (((0 <= k) && (k < j)) && (
($loc(new_array, k)).$c_ToDo == ($loc(
($Self).todos,
ii)).$c_ToDo)))))
invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> (
(($loc(new_array, ii)).$c_ToDo).$ToDo$completed ==
TODO())))
(($loc(new_array, ii)).$c_ToDo).$ToDo$state == TODO())))
invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> (
(($loc(new_array, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
{
if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed ==
TODO()))
if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == TODO()))
{
($loc(new_array, j)).$c_ToDo := ($loc(($Self).todos, i)).$c_ToDo;
j := (j + 1);
Expand Down
Loading
Loading