我想證明關於命令式面向對象程序的一些事實。如何在Coq中表示異構對象圖？我的主要問題是邊是隱含的 - 每個節點由整型標籤建模對象地址和模擬對象狀態的數據結構組成。所以隱式邊是由數據結構中的字段組成的，它們模擬對象指針幷包含圖中另一個節點的地址標籤。爲了確保我的圖形有效，向圖形添加新節點必須要求證明正在添加的數據結構中的所有字段都指的是圖形中已存在的節點。但是我怎樣才能在Coq中表達'數據結構中的所有指針字段'？在Coq中建模面向對象的程序
這取決於您如何表示數據結構以及要建模的語言具有哪些功能。這是一種可能性。假設您的語言有兩種值：數字和對象引用。我們所用的寫Coq的這種類型爲：
Inductive value : Type :=
| VNum (n : nat)
| VRef (ref : nat).
的引用（或指針）僅僅是可用於唯一地識別在堆中的對象的自然數。我們可以使用函數來表示兩個對象和堆如下：
Definition object : Type := string -> option value.
Definition heap : Type := nat -> option object.
在英語中複述，一個目的是從字符串（我們用它來模擬在對象字段）到值的部分功能，和堆是從nats（即對象引用）到對象的部分函數。然後，我們可以表達你的財產：
Definition object_ok (o : object) (h : heap) : Prop :=
forall (s : string) (ref : nat),
o s = Some (VRef ref) ->
exists obj, h ref = Some obj.
同樣，在英語：如果對象o領域s定義，並等於基準ref，則存在只會保存在該地址的一些對象obj堆h。
這種表示法的一個問題是Coq函數使得堆有無限多的對象，並且對象具有無限多的字段。您可以用另一種表示來繞過這個問題，該表示只允許在有限多個輸入上定義的函數，例如對的列表，或者（更好）一種有限映射的類型，如this one。