主要內容來自MIT6.031 Software Construction課程及HIT 軟件構造課程。
我們先來介紹兩種類型空間的值：
一、 Space of representation values （表示空間） R
表示空間由事實上實現的實體值構成。換句話說，由不同的、對抽象類型的實現的對象相應表示（Representation）的值組成。
二、 Space of abstract values (抽象空間） A
抽象空間由抽象類型設計支持的類型組成。直觀來說，就是抽象類型中設計的域或者說是支持變量。它們不是實際存在的實體，但是我們透過它們來理解抽象類型的元素。
一個例子：
我們在這個例子里我們使用字符串來表示字母的集合。
R和A之間的映射：
1. 每一個抽象空間的值都被映射到，是一個滿射（surjective）
2. 一些抽象類型的值被不止一個表示變量值映射，所以不是一個單射（not injective）
3. 不是所有表示變量值都在映射當中，不是一個雙射（not bijective）
抽象函數（Abstract Function）
抽象函數是表示從表示空間到抽象空間映射的函數
表示不變量（Rep Invariant）
表示不變量將表示變量值映射成一個布爾值。
可以將RI理解成一個表示值的子集，如果一個RI的值在到AF的映射當中，那么這個RI也就在這個子集當中，相應地，布爾值為真。