OpenGL图形规范的Z形式化描述

温晋杰，赵正旭

（石家庄铁道大学 信息科学与技术学院，河北 石家庄 050043）

OpenGL是图形硬件的一种软件接口，主要用于指定物体和对物体的操作，创建交互式的三维应用程序。如何对场景中的光照进行操纵，对于展示物体的三维特性，逼真地模拟现实世界意义重大。而Z语言是一种基于模型的形式化方法。其基本思想是利用一些已知的数学特性抽象来为目标软件系统的状态特征和行为特征构造模型。在需求规格说明中，Z语言精确的描述软件系统“做什么”而不涉及“怎么做”，只对目标软件系统进行功能描述。通过明确定义状态和操作来建立一个系统模型，特别适合于对无法进行现场调试的大型安全系统的描述。对应于系统抽象中的数据抽象和过程抽象，Z规范中有两种主要的模式状态模式和操作模式。通过状态转换的前、后置条件和输入输出变量之间应当满足的关系来描述操作。由于二者自身的特性，导致使用Z语言描述的OpenGL规范非常接近于OpenGL程序。

1 OpenGL

从生理学的角度上讲，眼睛之所以看见各种物体，是因为光线直接或间接的从物体表面到达了眼睛。人类对于光线强弱的变化的反应很大程度上表现了物体的立体感。如果没有光照，绝大多数物体看上去甚至像是一个二维物体。在OpenGL中，可以对场景中的光照和物体进行操纵，创建出丰富多彩的效果。OpenGL计算最终保存在帧缓冲区中每个像素的颜色取决于场景中所使用的光照以及场景中的物体是如何反射和吸收光线的［4］。OpenGL光照模型中的光照效果可以分为四个组成部分：Emitted（光源），Ambient（环境光），Diffuse（漫射光）和Specular（镜面反射光），最终结果由这四种光叠加而成。

OpenGL在模拟光照时，按照三原色的原理，将光分解为红、绿和蓝三种成分，所以光源的特征是由它所发出的红、绿、蓝三种光的数量来决定的。表面材料的特征是由它向各个方向反射的红、绿、蓝入射光的百分比决定的。在使用光照的时候主要分为以下三大步骤：

（1）创建和选择一个或多个光源，并设置光源的位置。

（2）创建和选择光照模型，它定义了全局环境光的等级和观察点的实际位置（用于光照计算）。

（3）设置场景中物体的材质属性。

本文使用形式化方法Z语言，针对上述给出的三大步骤进行详细的描述。

2 形式化方法Z

形式化方法Z是一种基于一阶谓词逻辑和集合论的规格说明语言。其中Z模式是它的基本结构，包括三个部分，模式名、变量的声明以及约束这些声明的谓词。也就是说模式等于声明加上谓词。模式有水平和垂直两种形式。由于模式的垂直模式更加容易理解，可读性比较强，所以，在本文当中，均采用垂直模式，如下所示：

在Z语言的早期发展阶段，它就被应用于实践，其中最著名的案例应该是IBM Hursley子公司利用Z语言对公司的用户信息管理系统进行了规格说明的重写，获得了成功，使得软件开发费用降低了9%。这对Z语言的发展产生了深远的影响。在国内Z语言的应用也有一些成果，例如在描述航天测控系统外测数据处理软件中的时标修正功能的测试用例中进行了应用，结果证明方法是严谨清晰的［6］。另外还有南京大学研制的COOZ－Tools和上海大学研制的Z User Studio等。1989年国际标准化组织公布了Z语言的正式标准。近几年，国家自然科学基金对Z研究课题都有资助。

3 光照规范的Z描述

3.1 定义类型和全程变量

在利用Z语言进行形式化规范描述的时候，可以根据不同的需求而选择不同的规范层次。在系统开发的初期，就要站在较高的一个角度来抽象系统规范，写出来的规范清晰易懂，随着过程的不断深入，我们着眼的角度应该逐渐降低，使得规范越来越接近于最终要实现的最低层次的规范［3］。本文将从集合、函数和序列的角度来对OpenGL光照规范进行Z形式化描述。

将OpenGL的光照规范光源、光照模型、材料属性和基本函数的状态集合。在该抽象层次上，暂定光源、光照模型、材料属性和函数为基本状态模式。规格说明使用以下基本数据类型：

［ARRAY，2F，BOOL］

BOOL：：＝0｜1，对应GL＿FALSE｜GL＿TURE；

ARRAY表示一个四元数组，

2F表示为双精度浮点数。

在下文中的描述中，以下两个构型是非常有用的。

3.2 系统状态模式的描述

系统状态模式的描述详见表1。

3.3 系统的初始化定义

初始化定义就是对系统所涉及的变量进行初始化，对变量赋予初始值，在初始化之前状态变量没有进行任何操作，所以初始化没有前状态（见表2）。

3.4 函数规范

（1）用于指定所有光源属性的函数是glLight（），它的三个参数决定了它所指定的是某个光源的属性、具体属性以及该属性的默认值（见表3）。

（2）光照模型的属性通过glLightModel（）函数来设置，该函数有两个参数，第一个表示要设置的项目，第二个参数表示属性要设置成的值（见表4）。

（3）材质与光源类似，也需要设置众多的属性（见表5）。材质属性通过glMaterial（）函数来设置，glMaterial（）函数有三个参数：第一个参数表示指定哪一面的属性，第二个指定了具体属性名，第三个参数表明该属性的具体值。

4 应用实例

通过一个模拟光照飞行器的实例，利用Z语言来描述OpenGL光照中函数的规范。通过二者的对比，来说明Z语言在描述OpenGL方面的优势（见表6）。

表1 定义光照参数

表2 初始化光照规范参数

表3 光源属性

表4 光照模型属性

表5 材料属性

表6 应用实例

在该实例中，依据Z语言的要求，从集合、函数、序列的角度对场景中飞行器添加光照效果的过程进行了Z形式化描述；输入集合均使用枚举类型，然后，通过Z标识符“seq”将输入的集合转换成相应的序列，其中，使用序列能够使得输入的属性和属性值相互对应，大大提高了描述的清晰性，准确性。通过对Z描述和OpenGL描述的对比，我们可以清晰地看到Z描述相对于其他非形式化描述方法的优势。整个软件开发的过程可以看成是从目标软件系统的规格说明出发，经过一系列步骤，每一步都增加一些可执行性或执行效率，最终达到程序代码的演化过程［1］。所以，我们对Z描述逐步求精和细化就可以得到可执行的OpenGL代码，十分准确，严谨。最终光照效果如图1所示。

图1 飞行器光照效果

5 结论

通过分析OpenGL图形标准光照规范的参数、函数关系，通过对规范的抽象化以及集合化，提炼出了一个适合于Z语言描述的光照效果添加过程。首先，对光源、光照模型、材质的参数和函数进行了一般性描述，最后通过对一个具体实例的描述，展示了Z形式化描述的优势。Z形式化描述目的是确保软件过程中描述的正确性和无二义性，因此形式化验证是实现形式化描述必不可少的过程。所以，形式化验证以及测试用例的自动生成将是进一步的研究目标。

［1］缪淮扣，李刚.软件工程语言—Z［M］.上海：上海科学技术文献出版社，1999.

［2］赵晓峰，赵正旭.基于Z的虚拟加工仿真环境规范技术研究［J］.系统仿真学报，2009，21（22）：7143－7146.

［3］赵晓峰，赵正旭.虚拟制造环境的信息规范及其Z描述研究［D］.山东：山东大学，2010.

［4］Dave Shreiner.The Khronos OpenGL ARB Working Group［M］.李军，徐波，译.北京：机械工程出版社，2010.1.

［5］刘玲，缪淮扣.Z规格说明构造方法［J］.计算机工程，2000，26（2）：39－41.

［6］王吉茂，尹平，张慧颖.基于Z语言的测试用例形式化描述方法研究［J］.计算机测量与控制，2013，21（12）：3175－3177.

［7］许庆国，缪淮扣，胡小波.Object－Z规格说明测试用例的自动生成器［J］.软件学报，2011，22（6）：1155－1168.