补充资料：Larch语言

Larch语言
Larch language

　　Larch yuyanLarch语言(Larch IangU剐罗)代数方法和一阶谓词方法相结合的形式软件规约语言簇，它旨在开发出各种技术和工具以支持形式规约的有效使用。肠rch语言由美国麻省理工学院J.V.Guttag等人于1983年提出。 1刁rell形式软件规约语言簇的主要目的是为各类程序设计语言的程序模块提供必要的描述手段，考虑到不同的程序设计语言常有不同的语法表示和语义定义，因而程序模块的规约就与某一特定的程序设计语言有关，为使和程序设计语言有关的特性局部化，助reh提供了描述各类程序设计语言的程序模块共性的共享语言和描述各个特定程序设计语言个性的接口语言。L盯eh语言簇中每一成员由共享语言及某一特定接口语言组成。 助rch共享语言采用代数方法，其描述单位为trait，提供一组供接口规约使用的类符和操作，由语法部分和公理部分组成。语法部分刻画了操作符的型构，公理部分以等式的形式给出。每一trait定义了一个相关的理论，作为它的语义，区别于常规的以模型作为语义的处理。trait定义中通过使用illlport俐includes子句以便从较小的如t组合成较大的trait，通过定义生成操作集和识别操作集扩展所定义的理论。1之reh共享语言的重要特征之一是引人多种语言成分以便于语义检查，trait中提供了mlplies子句用于表达用户希望相应trsit的理论所蕴涵的定理。 接口语言的目的是从软件规约的角度，将共享语言和特定的程序设计语言有机结合在一起，并提供描述程序模块中相应运算的机制。其中与特定语言有关的成分，如过程名、形式参数、类型、异常处理等描述的语法借助于该语言的语法，而其中过程的功能刻画用基于一阶谓词的前后断言的形式，描述中可以使用共享语言中trait的操作和类型。 1之reh语言通过区分共享语言和接口语言，使和程序设计语言有关的特性局部化，其共享语言具有易组合和强调语义检查的特点。共享语言采用代数方法，接口语言基于一阶谓词演算，具有较好的理论基础。 1刁reh已基于项重写系统实现，可用于分析其形式规约，检查其中的语义约束。I之reh语言已用于描述诸如图书馆系统等一系列软件规约。
　　

说明：补充资料仅用于学习参考，请勿用于其它任何用途。