Skip to content

Commit

Permalink
[motoko-san] rename field in todo_record.mo showcase
Browse files Browse the repository at this point in the history
  • Loading branch information
@GoPavel
GoPavel committed Jun 30, 2024
1 parent 4a9668c commit ca7663a
Show file tree
Hide file tree
Showing 2 changed files with 42 additions and 50 deletions.
58 changes: 25 additions & 33 deletions test/viper/ok/todo_record.vpr.ok
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,7 @@ 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
Expand Down Expand Up @@ -79,7 +78,7 @@ 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)
Expand Down Expand Up @@ -120,7 +119,7 @@ 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;
Expand Down Expand Up @@ -200,10 +199,9 @@ 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 (($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)
Expand All @@ -213,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 @@ -234,7 +232,7 @@ 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;
Expand All @@ -256,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 Down Expand Up @@ -306,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 @@ -321,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 @@ -330,22 +327,19 @@ 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))
Expand All @@ -366,19 +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
34 changes: 17 additions & 17 deletions test/viper/todo_record.mo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ import Prim "mo:⛔";
import Array "mo:base/Array";

actor Assistant {
type ToDo = { id: Nat; desc: Text; completed: State };
type ToDo = { id: Nat; desc: Text; state: State };
public type State = { #TODO; #DONE };

var todos : [var ToDo] = [var ];
Expand All @@ -29,7 +29,7 @@ actor Assistant {
(0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
if (n <= todos.size())
return;
let new_array = Array.init<ToDo>(n, { id = 0; desc = ""; completed = #TODO });
let new_array = Array.init<ToDo>(n, { id = 0; desc = ""; state = #TODO });
var i: Nat = 0;
while (i < todos.size()) {
// actor invariant:
Expand Down Expand Up @@ -60,7 +60,7 @@ actor Assistant {
// assert:return Prim.forall<Nat>(func i =
// (0 <= i and i < (old(todos.size())) implies todos[i] == Prim.Ret<[ToDo]>()[i]));
// let new_array = Array.tabulate<(Nat, Text, State)>(num, func i = todos[i]);
let new_array : [ToDo] = [ { id = 0; desc = ""; completed = #TODO } ];
let new_array : [ToDo] = [ { id = 0; desc = ""; state = #TODO } ];
return new_array;
};

Expand Down Expand Up @@ -104,14 +104,14 @@ actor Assistant {
assert:return num == (old(num)) + 1;
assert:return nextId == (old(nextId)) + 1;
assert:return Prim.Ret<Nat>() == (old(nextId));
assert:return todos[num-1] == ({ id = Prim.Ret<Nat>(); desc = description; completed = #TODO });
assert:return todos[num-1] == ({ id = Prim.Ret<Nat>(); desc = description; state = #TODO });
assert:return Prim.forall<Nat>(func i =
(0 <= i and i < num-1 implies todos[i] == (old(todos[i]))));
let id = nextId;
if (num >= todos.size()) {
resize(num * 2+1);
};
todos[num] := { id = id; desc = description; completed = #TODO };
todos[num] := { id = id; desc = description; state = #TODO };
num += 1;
nextId += 1;
return id;
Expand All @@ -123,7 +123,7 @@ actor Assistant {
assert:return Prim.forall<Nat>(func i =
((0 <= i and i < num and todos[i].id != id) implies todos[i] == (old(todos[i])) ));
assert:return Prim.forall<Nat>(func i =
((0 <= i and i < num and todos[i].id == id) implies todos[i].completed == #DONE ));
((0 <= i and i < num and todos[i].id == id) implies todos[i].state == #DONE ));
var i : Nat = 0;
while (i < num) {
// actor invariant
Expand All @@ -139,12 +139,12 @@ actor Assistant {
assert:loop:invariant Prim.forall<Nat>(func ii =
(0 <= ii and ii < i and todos[ii].id != id implies todos[ii] == (old(todos[ii]))));
assert:loop:invariant Prim.forall<Nat>(func ii =
(0 <= ii and ii < i and todos[ii].id == id implies todos[ii].completed == #DONE));
(0 <= ii and ii < i and todos[ii].id == id implies todos[ii].state == #DONE));
// let (taskId, taskDesc, _) = todos[i]; // TODO: requires recursive patterns
switch (todos[i]) {
case({ id = taskId; desc = taskDesc; /* _ */completed = (_completed: State) }) {
case({ id = taskId; desc = taskDesc; /* _ */state = (_state: State) }) {
if (taskId == id) {
todos[i] := { id = taskId; desc = taskDesc; completed = #DONE };
todos[i] := { id = taskId; desc = taskDesc; state = #DONE };
};
i += 1;
};
Expand All @@ -171,25 +171,25 @@ actor Assistant {
((0 <= ii and ii < num) implies todos[ii] == (old(todos[ii])) ));
let todo: ToDo = todos[i];
output := output # "\n" # todo.desc;
switch (todo.completed) {
switch (todo.state) {
case (#DONE) { output := output # " ✔"; };
case (#TODO) { output := output # " ❌"; };
}
};
return output # "\n";
};
public func clearCompleted() : async () {
public func clearstate() : async () {
assert:return num <= (old(num));
assert:return nextId == (old(nextId));
assert:return todos.size() == (old(todos.size()));
assert:return Prim.forall<Nat>(func i =
(0 <= i and i < (old(num)) and (old(todos[i].completed)) == #TODO
(0 <= i and i < (old(num)) and (old(todos[i].state)) == #TODO
implies Prim.exists<Nat> (func k =
( 0 <= k and k < todos.size() and todos[k] == (old(todos[i])) )) ));
assert:return Prim.forall<Nat>(func i =
(0 <= i and i < num implies todos[i].completed == #TODO));
let new_array = Array.init<ToDo>(todos.size(), { id = 0; desc = ""; completed = #TODO });
(0 <= i and i < num implies todos[i].state == #TODO));
let new_array = Array.init<ToDo>(todos.size(), { id = 0; desc = ""; state = #TODO });
var i: Nat = 0;
var j: Nat = 0;
while (i < num) {
Expand All @@ -207,13 +207,13 @@ actor Assistant {
assert:loop:invariant j <= i;
assert:loop:invariant 0 <= j and j <= num;
assert:loop:invariant Prim.forall<Nat>(func ii =
(0 <= ii and ii < i and todos[ii].completed == #TODO
(0 <= ii and ii < i and todos[ii].state == #TODO
implies Prim.exists<Nat>(func k =
(0 <= k and k < j and new_array[k] == todos[ii] ))));
assert:loop:invariant Prim.forall<Nat>(func ii =
(0 <= ii and ii < j implies new_array[ii].completed == #TODO ));
(0 <= ii and ii < j implies new_array[ii].state == #TODO ));
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < j) implies new_array[ii].id < nextId);
if (todos[i].completed == #TODO) {
if (todos[i].state == #TODO) {
new_array[j] := todos[i];
j += 1;
};
Expand Down

0 comments on commit ca7663a

Please sign in to comment.