简介
形式规范
多年来，学术界一直在试图通过使用与测试截然不同且更加主动的方法来确保程序语义的正确执行：形式化方法。研究者们认为这种方法通过更加精确、无二义性的描述来达到让程序绝对地按照设计者的思想执行的目的。这种思想早期体现在Floyd在1967年提出的程序的部分正确性的证明上。在后来的几十年中，这种思想不断发展，人们开始不单单注重静态的模型似的形式化语义，动态可执行的并发语义也随之出现。
ADL
形式架构定义语言（Architecture Description Language, ADL）是一种用于描述软件系统的架构的正式语言。ADL 的主要目的是通过提供一种标准化的方式来描述软件系统的结构、组件及其交互，从而帮助设计者和开发者更好地理解和管理复杂的软件系统。ADL 通常用于系统架构设计、分析和验证，尤其是在大型和复杂系统中。
使用形式架构定义语言(ADL)对架构进行描述可以辅助对高层设计进行规范和分析。例如，架构模型可以用来分析证明死锁的存在，或用来决定安全的信息是否流入到不安全的模块中去。架构模型也在软件生产线的建设中起着重要作用。
ADL 的典型元素
-
组件（Component）：
- 定义：系统的基本构建块，可以是软件模块、服务、数据库等。
- 属性：组件可以有属性，如名称、类型、版本等。
- 接口：组件对外提供的接口，定义了组件可以接收和发送的消息或数据。
-
连接件（Connector）：
- 定义：描述组件之间的交互机制，如消息传递、数据流等。
- 属性：连接器可以有属性，如类型、协议等。
- 行为：连接器可以定义其行为，如同步或异步通信、事务管理等。
-
架构配置（Arch Configuration）：
- 定义：描述系统中组件和连接器的实例化和组装方式。
- 属性：配置可以有属性，如名称、版本等。
- 关系：配置定义了组件之间的关系和连接器的使用。
两类ADL
目前存在的ADL在对架构与具体实现的处理方式上主要可以被分为两大类。
第一类的ADL 只定义抽象，而与具体的实现语言的结合过于松散，致使软件在分析、实现、理解与系统进化出现严重的问题。一些ADL往往附带一些自动生成代码的工具，这些生成的代码可以连接起独立开发的组件。然而，这些ADL却没有提供任何使这些组件遵循系统架构限制的保证，相反的是，它们依赖于组件的开发者来遵循规范。另外一些ADL只能作为纯建模和分析工具；它们不提供任何工具来生成代码，仅仅要求程序员在没有任何自动化工具的辅助下生成代码。因此在实现中反映架构相当困难。最重要的一个问题就是这些系统都无法保证通讯完整性原则（Communication Integrity），从而尽管架构被用来分析和建模，但并无任何方法知道实现中是否已经完全遵循架构的设计。
与第一类的ADL完全相反，第二类以ArchJava为代表的ADL用强大的 类型系统（type system）来保证实现对架构限制的遵守，如ArchJava将架构与实现统一在一种语言中，使用语言级别的类型检查（type checking）来强制执行。目前存在的ADL中，唯一可以保证通讯完整性的只有ArchJava语言。然而ArchJava并不是单纯的描述语言，它牵涉了更多的实现细节，因此无法提供给架构设计师使用进行最初的系统架构分析和设计，因为在设计阶段，细节代码并不存在。
组件及组件接口的形式化描述
以JML为例，Java Modeling Language 是美国 Iowa State University (ISU) 计算机系程序设计语言与形 式化方法实验室为 Java 语言所设计的行为接口规范语言 (BISL)。它采用了类似于 Java 的语法结构，从而使其更容易被 Java 程序员所接受。
JML允许对类的不变式(Invariant)，前置谓词(pre-condition)与后置谓词(post-condition)进行规范。每一规范语句由布尔类型的Java表达式所组成，并以注释形式（//@ 或 /*@....@*/）出现在Java程序中。@ 符号是为了使得JML解释器能够识别。
一段简单的JML代码如下所示：
/*@ public normal_behavior
@ requires P;
@ ensures Q;
@*/这段代码为类中一个声明为公共的方法进行了规范：此方法执行前必须满足条件P，结束后必须保证布尔表达式Q成立。同时，此方法必须正常结束，无异常抛出。
一个使用 JML 进行形式规范说明的实例
连接件的形式化描述
JCMPL 是一种仅定义抽象的新型的架构定义语言，其最大特点就在于在显示指定架构中组件存在及其关系的同时，能够最大程度地支持组件独立开发及最终的第三方集成。在连接组件中未知接口时，JCMPL 使用通配符 * 来表达这个接口。
JCMP工具在编译JCMPL生成目标Java代码的时候，遵循了triple-C模式，即组件间使用软件连接器（software connector）进行通信的传递，而并非通常的直接Client-Server调用关系。
在基于triple-C模式的实现中，软件连接件（Software Connector）被用来实现架构中的组件间的连接。作为组件集成适配器以及方法调用的代理，Connector负责被连接的组件端口中的方法匹配和方法间的数据传输。由于Connector所处在这样一个特殊的位置，所有接口方法及数据对其都是透明的，这也产生了对数据进行智能分析以及自动化进行组件匹配的可能性。作者根据Connector的这一特性，开发了JCMP/Match试图对连接在一起的组件端口中的方法进行自动匹配，找出最有可能的需求-供应方法对。
架构配置
架构配置是构件和连接件的结构性组合，定架构配置描述了系统中所有构件和连接件的组织和布局方式。"义了系统的整体架构。
配置可以包括对构件和连接件的实例化、部署以及它们之间的连接关系。它确保系统按照既定的架构原则和模式组装和运行。
