From ef6dc3e27d7e09f7631726d11c67dfb962867f75 Mon Sep 17 00:00:00 2001 From: Pavel Golovin Date: Mon, 1 Jul 2024 01:55:14 +0200 Subject: [PATCH] [motoko-san] rename field in todo_record.mo showcase --- test/viper/ok/todo_record.vpr.ok | 58 ++++++++++++++------------------ test/viper/todo_record.mo | 34 +++++++++---------- 2 files changed, 42 insertions(+), 50 deletions(-) diff --git a/test/viper/ok/todo_record.vpr.ok b/test/viper/ok/todo_record.vpr.ok index 5918ca84d3e..9bbb49c6e01 100644 --- a/test/viper/ok/todo_record.vpr.ok +++ b/test/viper/ok/todo_record.vpr.ok @@ -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 @@ -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) @@ -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; @@ -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) @@ -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; @@ -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; @@ -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); }; @@ -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); }; @@ -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) @@ -330,14 +327,11 @@ 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 @@ -345,7 +339,7 @@ method clearCompleted($Self: Ref) 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)) @@ -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); diff --git a/test/viper/todo_record.mo b/test/viper/todo_record.mo index d6d1ae74ba6..02f317b5c51 100644 --- a/test/viper/todo_record.mo +++ b/test/viper/todo_record.mo @@ -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 ]; @@ -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(n, { id = 0; desc = ""; completed = #TODO }); + let new_array = Array.init(n, { id = 0; desc = ""; state = #TODO }); var i: Nat = 0; while (i < todos.size()) { // actor invariant: @@ -60,7 +60,7 @@ actor Assistant { // assert:return Prim.forall(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; }; @@ -104,14 +104,14 @@ actor Assistant { assert:return num == (old(num)) + 1; assert:return nextId == (old(nextId)) + 1; assert:return Prim.Ret() == (old(nextId)); - assert:return todos[num-1] == ({ id = Prim.Ret(); desc = description; completed = #TODO }); + assert:return todos[num-1] == ({ id = Prim.Ret(); desc = description; state = #TODO }); assert:return Prim.forall(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; @@ -123,7 +123,7 @@ actor Assistant { assert:return Prim.forall(func i = ((0 <= i and i < num and todos[i].id != id) implies todos[i] == (old(todos[i])) )); assert:return Prim.forall(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 @@ -139,12 +139,12 @@ actor Assistant { assert:loop:invariant Prim.forall(func ii = (0 <= ii and ii < i and todos[ii].id != id implies todos[ii] == (old(todos[ii])))); assert:loop:invariant Prim.forall(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; }; @@ -171,7 +171,7 @@ 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 # " ❌"; }; } @@ -179,17 +179,17 @@ actor Assistant { 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(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 (func k = ( 0 <= k and k < todos.size() and todos[k] == (old(todos[i])) )) )); assert:return Prim.forall(func i = - (0 <= i and i < num implies todos[i].completed == #TODO)); - let new_array = Array.init(todos.size(), { id = 0; desc = ""; completed = #TODO }); + (0 <= i and i < num implies todos[i].state == #TODO)); + let new_array = Array.init(todos.size(), { id = 0; desc = ""; state = #TODO }); var i: Nat = 0; var j: Nat = 0; while (i < num) { @@ -207,13 +207,13 @@ actor Assistant { assert:loop:invariant j <= i; assert:loop:invariant 0 <= j and j <= num; assert:loop:invariant Prim.forall(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(func k = (0 <= k and k < j and new_array[k] == todos[ii] )))); assert:loop:invariant Prim.forall(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(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; };