在Coq中建模面向对象的程序 [英] Modelling object-oriented program in Coq

问题描述

我想证明关于命令式面向对象程序的一些事实。如何在Coq中表示异构对象图？我的主要问题是边是隐含的 - 每个节点由整型标签建模对象地址和模拟对象状态的数据结构组成。所以隐式边是由数据结构中的字段组成的，它们模拟对象指针并包含图中另一个节点的地址标签。为了确保我的图形有效，向图形添加新节点必须要求证明正在添加的数据结构中的所有字段都指的是图形中已存在的节点。但是我怎样才能在Coq中表达'数据结构中的所有指针字段'？解析方案

这取决于你如何表示一个数据结构以及要建模的语言具有哪些功能。这是一种可能性。假设您的语言有两种值：数字和对象引用。我们可以将这种类型写入Coq中：

 归纳值：类型：= 
 | VNum（n：nat）
 | VRef（ref：nat）。 
  

引用（或指针）只是一个自然数，可用于唯一标识堆。我们可以使用函数来表示对象和堆，如下所示：

 定义对象：类型：= string  - >期权价值。 
定义堆：类型：= nat  - >选项对象。 
  

在英语中，一个对象是一个来自字符串的部分函数（我们用它来模拟字段对象）为值，而堆是从nats（即对象引用）到对象的部分函数。然后，我们可以表达你的财产：

 定义object_ok（o：object）（h：heap）：Prop：= 
 forall（s：string）（ref：nat），
os = Some（VRef ref） - > 
存在obj，h ref =一些obj。 
  

同样，如果字段 s 对象 o 被定义，并且等于引用 ref ，那么存在一些对象 obj 存储在堆上的该地址 h 。

这种表示就是Coq函数使得堆有无限多的对象，并且对象拥有无限多的域。你可以用另一种表示来绕过这个问题，这种表示只允许定义在有限多个输入上的函数，比如成对的列表，或者（甚至更好）一类有限映射，比如这一个。

I want to prove some facts about imperative object-oriented program. How can I represent a heterogeneous object graph in Coq? My main problem is that edges are implicit - each node consists of an integer label modelling object address and a data structure that models object state. So implicit edges are formed by fields inside data structure that model object pointers and contain address label of another node in a graph. To ensure that my graph is valid, adding new node to the graph must require a proof that all fields in a data structure that is being added refer to nodes that already exist in the graph. But how can I express 'all pointer fields in a data structure' in Coq?

解决方案

It depends on how you represent a data structure, and what kinds of features the language you want to model has. Here's one possibility. Let's say that your language has two kinds of values: numbers and object references. We can write this type in Coq as:

Inductive value : Type :=
| VNum (n : nat)
| VRef (ref : nat).

A reference (or pointer) is just a natural number that can be used to uniquely identify objects on the heap. We can use functions to represent both objects and the heap as follows:

Definition object : Type := string -> option value.
Definition heap : Type := nat -> option object.

Paraphrasing in English, an object is a partial function from strings (which we use to model fields in the object) to values, and a heap is a partial function from nats (that is, object references) to objects. We can then express your property as:

Definition object_ok (o : object) (h : heap) : Prop :=
  forall (s : string) (ref : nat),
    o s = Some (VRef ref) ->
    exists obj, h ref = Some obj.

Again, in English: if the field s of the object o is defined, and equal to a reference ref, then there exists some object obj stored at that address on the heap h.

The one problem with that representation is that Coq functions make it possible for heaps to have infinitely many objects, and objects to have infinitely many fields. You can circumvent this problem with an alternative representation that only allows for functions defined on finitely many inputs, such as lists of pairs, or (even better) a type of finite maps, such as this one.

这篇关于在Coq中建模面向对象的程序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！