计算机语言是计算机与使用者之间的通讯语言。是计算机与其使用者之间信息传递的媒介。　　计算机语言的发展经历了最初的低级语言到高级语言的复杂历程。由最初的机器语言到二进制编码的低级语言再到后来的面向过程的高级语言以至目前流行的面向对象的编程语言。规约语言是计算机学科领域中的一种形式化语言。它不同于一般的编程语言,形式语言一般用于系统的分析和设计中,从而使得开发思想更容易理解。程序切片是源起于程序调试的一门新兴的理论,目前在软件开发的各个阶段都有应用,比如软件测试、软件度量、软件重用等。本文基于对UML形式化的研究和程序切片精度问题的研究做了以下几点工作:　　(1)通过形式化规约语言Z将UML的部分模型图进行了形式化描述,一定程度上避免了模型图语义的二义性。　　本文主要讨论统一建模语言UML的形式化描述。随着软件工程概念的提出,各种方法学的不断融合,统一建模语言UML从各种建模语言中脱颖而出。UML是一种图形符号系统,主要通过九种侧重点不同的模型图对系统进行描述。虽然它是一种系统描述语言,但是由于它本身的特点,造成了它在系统规格描述方面会产生一定的二义性。图形符号系统和自然语言对规格说明描述上虽然具有直观易理解的特性,但是由于自然语言不可避免的歧义性导致规格描述时的歧义性,本文通过一种形式语言Z的描述规格对UML模型进行形式化转换。从而为系统的模型验证提供依据。　　(2)通过对基于规约切片的研究,给出一种计算基于规约的切片的算法,提高切片本身的精度。　　程序切片作为一门新兴的理论,起源于程序调试,目前比较成熟的应用在软件测试中,有很多学者尝试将其应用于软件开发过程的各个阶段并且取得了一定的进展。作为一种理论基础或者应用工具,切片本身的精度的保证是很重要的问题。本文主要对基于规约的切片进行研究,基于有条件切片算法,给出了一种计算基于规约的切片算法。保证了程序切片在给定前置后置条件基础下能够保证获得的切片是最小的,精度也最高。　　(3)通过对规约切片和UML模型图的形式化描述,探讨了将程序切片理论用于UML规约中,一定程度上避免了模型图语义的二义性。　　(4)在文章的第五章提出了将切片思想运用到UML模型规约中的两点想法:第一点是对软件模型结构进行切片获取“部分语义”的子模型结构,对提高原型系统的构造效率有一定的帮助。第二点是将UML的用例图形式化描述中的前后置条件与基于规约的切片思想融合,通过这种思想获取用例图的切片,从而为模型验证提供新途径。第四点工作是本文需要进一步深入的部分。