如何解决编写类似 c 的类以在 Coq 中运行
我正在尝试为 coq 中的一个简单的类似 c 的程序提出一种语法和语义。这是一门关于编程语言原理的大学课程。
我在网站上查看了类似的问题,只找到了两个接近我需要的主题,但它们与我需要做的并不完全相同。
长话短说,我目前有一个类的定义:
Inductive Object :=
| object : string -> list_variable -> Function -> Object.
list_variable 声明为:
Inductive list_variable : Type :=
| null
| cons (s : string) (l : list_variable).
和函数声明为:
Inductive Function :=
| function : string -> list_variable -> Function.
所有这些都应该包含在下面的语句中,我需要用它来构建一些应该无错误运行的测试程序:
Inductive Stmt :=
| var_declare : string -> Stmt
| object_declare : Object -> string -> Stmt
| function_declare : function -> Stmt -> Stmt
| assignment : string -> Exp -> Stmt
| sequence : Stmt -> Stmt -> Stmt
| ifthenelse : Exp -> Stmt -> Stmt -> Stmt
| ifthen : Exp -> Stmt -> Stmt
| while : Exp -> Stmt -> Stmt.
Exp 只是一个包含变量、数字、算术和布尔表达式的归纳类型。
我的问题是,如何模拟类似内存的环境,在其中定义对象、为所述对象创建实例并至少能够访问特定实例的成员变量?
我得到了一些恢复使用两个映射的提示,一个从变量(或对象)到内存地址,另一个从内存地址到值。所以,它应该是这样的形式:
Definition Address := Object -> ObjAddress.
Definition ObjValues := Address -> Value (nat,bool or string)
最后,我想有以下几点:
class example {member variables and methods};
example e1;
e1.variable=1.
对于如何将其编码到 coq 中,您有什么想法吗?
解决方法
“类c”(如您所说)语言,我认为是一种存在别名问题的语言,即您可以对同一内存位置进行多次引用,并且引用可以具有不同类型.但是您似乎没有变量的类型声明。也许您的语言中只有 int
?
C 也有一个堆栈和一个堆以及可以指向其中任何一个的指针,因此当函数返回时,别名引用可能会变得无效。您的语言似乎也没有指针或 malloc,因此您的语言可能不必处理。
但如果你真的想这样做,那么我建议你看看 CompCert
是如何完成的,它有一种漂亮的记忆建模方式。 The CompCert Memory Model,Version 2
但是如果您 don't
想要处理所有这些混乱和别名(我认为这是您真正想到的),那么您可以将内存建模为函数 mem
从变量名到值 (nat
)。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。