文件名称：actario:Coq上的Actor系统验证框架
文件大小：326KB
文件格式：ZIP
更新时间：2024-05-29 02:22:38
OCaml
阿塔里奥 Actario是一个框架，用于在Coq上形式化和验证Actor系统。 该项目正在开发中。 Actario =演员+场景 要求 Coq-8.8 mathcomp-1.7 安装 $ cd /path/to/actario $ ./configure $ make $ make install 例子 参见 。 当前状态 Actor模型的语法和语义的形式化 语法： new ， send ， self ， become （theory / syntax.v， actions ） 语义：标记的过渡语义（theory / semantics.v， trans ） 方便的符号理论/语法 演员姓名无重复的证明 理论/ trans_invariant.v（ initial_trans_star_no_dup ） 验证Actor系统的机制/逻辑 配置之间的通讯 提取到Erlang