广谱语言(wide spectrum language)是指可在不同的抽象级别上书写软件需求定义、功能规约、设计规约及实现的语言。好的软件规约要在较高的抽象级上说明做什么,强调明晰,而好的实现必须针对虚拟机给出如何做的详细描述,强调功效。明晰与功效很难在一个程序同时满足,这两者之间距离很大。程序规约在这个距离间分成若干个抽象级别。光谱语言及其相应的支撑系统能够在同一个语言架构下明晰的规约通过推理逐步向高效的程序转化,或者提供低级别相对高级规约的正确性证明的辅助手段。
简介
算法设计自动化是软件自动化的核心和难点所在,其含义是:从“做什么”的软件功能规格说明自动或半自动地生成“如何做”的软件设计规格说明直至机器可执行的程序。传统的规格说明语言和程序设计语言由于结构单一而难以适应算法设计自动化的需要。因此,必须设计一种能够刻划软件功能规格说明、软件设计规格说明、可执行程序以及相应算法设计过程的广谱语言。光谱语言是指提供规约级到实现级的数据结构和控制结构的构造,并提供结构间语义等价的转换规则,用于自动转换或验证低级结构的相对高级结构的正确性的语言。典型代表语言CIP-L语言。
特点
广谱性:广谱性是指语言既能刻化“做什么”的功能规格说明,又能表达“如何做”的设计规格说明与可执行程序,并能反映其间的转换过程。
紧耦合性:紧耦合性是指语言中多种语言层次的语言成分必须具有统一的语法表示和共同的语义基础,而不是简单地将各种语言成分组合在一起。
严密性:严密性是指语言具有良好的数学基础,便于转换过程的语义分析和自动实现。
实用性:实用性是指语言结构简明与表示方便,其数学背景尽量对用户隐蔽,便于学习和使用1。
需求问题表示的需要
软件规格说明语言区别于传统程序设计语言的本质是其面向问题的特征,即它能简明而清晰地表达待解问题而不必涉及问题的求解过程与功效。问题表示的多样性导致软件规格说明的广谱性。前后断言是一种用于刻划软件功能的形式化方法,在可以随意使用谓词的情况下,前后断言可以清晰而方便地描述各种问题。然而,基于前后断言方法的软件规格说明语言所能提供的基本谓词集是有限的。为使这样有限的基本谓词集能满足前后断言方法刻划软件功能的需要,途径之一是采用构造性的方法。提供一定的结构手段,如各种逻辑联结词和量词,使之能对基本谓词加以组合而构成新的满足需要的谓词,这一途径的难点在于提供具有一定抽象级别的、通用的、便于自动化的、有限的、相对完备的基本谓词集;并且对于刻划大型软件来说,复杂的逻辑公式特别难以书写和理解。大型软件的主要特征是其复杂性,而分解和抽象是克服复杂性的两个关键手段,在某种意义下,功能规格说明具有抽象性,而分解手段具有设计性。因此,有必要将功能规格说明与设计规格说明有机地结合起来。途径之二是面向特定的应用领域,即提供面向特定应用领域的相对完备的基本谓词集;这条途径我们在设计FGSPEC语言中已进行了初步尝试,结果表明:确定合适的范围与相关的基本谓词取决于对特定应用领域的透彻理解。并且,对于某些问题,特别是超出领域的用归纳方式定义的问题(如求阶乘)等,如无专用谓词,便难以刻划。因此,必须提供设计规格说明作为功能规格说明的补充手段,使语言具有较强的表达能力。
刻划算法设计过程的需要
传统的程序设计语言为了增加程序的易读性,曾试图用程序正文来反映程序设计过程,但未能奏效。主要问题在于单一的程序正文难以权衡表示的清晰性和实现的功效性,更难以反映其间的转换过程。这就要求规格说明语言不仅能刻划“嵌什么”的功能规格说明与“如何做,的设计规格说明,而且还必须能刻划其间的转换过程。亦即,要求具有广谱性,以此作为研究和实现算法设计自动化的基础。
实现算法设计自动化的需要
和传统的编译实现技术不同,算法设计自动化的实现涉及多层次语言间的转换,如从功能性的规格说明到设计性的规格说明以及从设计性的规格说明到可执行的程序,如果对不同层次设计不同的语言,那么,一方面,多种语言需多种分析程序,增加了实现的负担;另一方面,由于各语言层次间的转换,特别是从功能规格说明到设计规格说明的完全自动转换尚难做到,因此,须有人工千预。如果在规格说明语言中不能反映其间的逐步转换过程,使人和实现系统在统一的转换模式下进行算法设计,则势必使用户要了解自动化系统的内部细节,不便于人机交互。
CIP-L语言
CIP-L语言(CIP-L language)是一种支持转换 式程序设计的广谱语言。CIP-L可描述从软件功能 规约、设计规约、作用式程序到过程式或面向机器的 高效程序等不同的抽象级;提供了从高抽象级向低 抽象级转换的语言结构和语义规则。它是70年代 中期由德国慕尼黑技术大学F.L.Bauer主持开发的“直觉引导的计算机辅助程序设计”项目的主要部分,用以支持转换式程序设计方法,保证程序转换的正确性。 作为广谱语言,CIRL用代数类型描述功能规约,用计算结构刻画代数类型的模型,用模式描述算法和控制结构。代数类型也就是抽象数据类型,其公理用一阶逻辑公式表示。CIP-L要求,代数类型中的任一对象均可经有限步基本运算生成。这种生成结构可用CIP-L的计算结构刻画。模式是一个算法架构,用以描述算法策略和控制策略,将一个模式中的代数类型名赋予具体的语义解释后即可得到具体的算法。模式语言又分成核心层和多个扩展层。 核心层定义了表达式子语言,可按逻辑式或函数式风格书写程序,采用模型论方法定义其语义。扩展层包含了申述式子语言,命令式子语言,并行子语言和控制子语言,它们的语义刻画采用转换语义方法,即每一语法结构的语义均可由转换规则在有限步内归结到核心层语义。 CIP-L针对转换式程序设计的需要而设计。语 言覆盖了从功能规约到过程实现各个层次,功能很 ,但同时造成结构繁杂,不易掌握。
本词条内容贡献者为:
王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所