Page 159 - 《软件学报》2025年第8期

3582 软件学报 2025 年第 36 卷第 8 期

● 递归函数必须终止.
首先, 我们定义了 wellform_descendents 断言来说明当前节点与后代节点构成树状结构, 它需要一个辅助函
数 wellform_descendents_list, 通过互递归定义.

wellform_descendents:
| wellform_descendents_cons:
forall map node ls listchild,
wellform_descendents_list (child node ls map) listchild ls map →
contains listchild node = false →
wellform_descendents node (node :: listchild) ls map
with wellform_descendents_list:
| wellform_descendents_list_leaf:
forall ls map, wellform_descendents_list nil nil ls map
| wellform_descendents_list_cons:
forall node desc1 rest listchild1 listchild2 ls map,
wellform_descendents node desc1 ls map →
wellform_descendents_list rest listchild2 ls map →
intersection listchild1 listchild2 = false →
wellform_descendents_list (node :: rest) (listchild1 ++ listchild2) ls map.

wellform_descendents_list 表示一个列表中的所有节点都满足后代无环的性质. wellform_descendents 定义中,
断言 contains listchild node 为 false, 说明当前节点的后代节点列表中不包含当前节点, 从而说明当前节点和后代节
点组成一个树状结构. 在 wellform_descendents_list 的定义中, 调用 wellform_descendents 来表示当前加入的节点
node 满足后代无环性质, 并且 node 的后代与 rest 列表的后代集合没有交集, 构成了一个由多个树组成的森林结
构. 两者相互调用定义了后代无环的性质, 从而可以保证函数的递归执行总是可以终止的.
每个权能节点都应该和后代权能节点构成一个树状结构, 这在权能不变式 CapabilityInv 中得到保证: 不变式
中的断言 capability_wellform_descendents 定义为, 系统中每个权能节点都满足 wellform_descendents 性质, 从而保
证每个权能节点都满足无环性质.
然后, 我们定义了断言 reset_descendents_cspace_slot 来描述每次撤销操作前后权能空间所满足的性质, 表示
撤销单一节点及其所有后代节点的对应权能. 同样它的定义需要互递归断言 reset_descendents_cspace_list_slot 来
协助完成, 表示对于一个节点列表的所有结点及其后代的对应权能进行撤销. 断言 reset_descendents_cspace_slot
恰好定义了 deleterec 函数中 while 循环的不变式.
有了上述定义, 我们很容易建立内核函数 deleterec 和 cnode_revoke_kernel 的前后条件规范, 这里由于篇幅原
因省略了.
最后, 我们列出 API 函数 cnode_revoke 的抽象规范, 形式如下.

cnode_revoke_spec(vl: vallist) :=
cnode_revoke_invalid(vl) ?? /*失败的规范*/
…/*失败的规范*/
cnode_revoke_success(vl). /*成功的规范*/
其中, ??代表 cnode_revoke 函数执行结果的不确定性, 表示可能发生多种情况. 前几种规范代表执行失败情况的集
合, 最后一种代表执行成功的规范. 以下将以成功的情形介绍为其建立的抽象规范. cnode_revoke_success 表示成
功情形, 它对高层抽象状态进行修改, 返回 success.