Page 287 - 《软件学报》2026年第3期

1250 软件学报 2026 年第 37 卷第 3 期

(1) 变更历史包括变更日期、变更内容和变更原因.
(2) 应用情况包含软件 IP 的运行记录, 例如该 IP 在哪些领域的哪些项目中进行了使用.

4 软件 IP 的形式模型

形式化方法是全面系统地使用基于数学的语言、技术和工具精确地说明、开发和验证软件系统, 使用形式化
方法描述的规约具有规范性和无二义性. 采用形式化方法描述软件 IP 可以最大程度地减少软件 IP 创建者和使用
者对软件 IP 的认知差距, 有利于正确地理解软件 IP 的含义, 为基于软件 IP 的软件智能合成提供安全性保障. 一
般地, 给定一个程序 M, 根据 Floyd-Hoare 逻辑, 它的形式模型可以表示为一个 Hoare 三元组: {p}M{q}, 其中 p 表
示 M 输入满足的性质 (前置条件), q 表示 M 执行之后输出满足的性质 (后置条件). 前后断言 (p, q) 定义了程序 M
的形式规约. 另外, 不变式也是描述程序满足的性质的重要手段. 程序不变式与程序的前后断言 (p, q) 不同: (p, q)
描述程序输入和输出的性质, 它不关注程序执行过程; 而不变式则描述了程序在运行过程中, 程序的状态始终满足
的约束. 通过不变式可以证明程序满足的性质 (例如可终止性等). 对于嵌入式软件, 除了它的功能行为, 我们通常
也关注它的非功能行为 (例如性能、资源要求、安全性、健壮性等) 的形式描述, 即非功能约束. 综上所述, 对于
软件 IP 形式模型, 可以定义以下三元组:
FM = (Spec, NonFun, Inv),
其中, Spec 表示形式规约, NonFun 表示非功能约束, Inv 表示 IP 不变式.
4.1 形式规约
以上提到的前后断言 (p, q) 定义了程序的形式规约, 又称为程序的契约. 实际上, 这种基于契约的设计 (DbC)
思想正是来源于 Floyd-Hoare 逻辑. 基于契约的设计方法能够独立地描述每个 IP 的责任以及对 IP 所需环境的假
设, 检查 IP 之间组装时是否相容、一致, 从而保证组装后系统的正确性, 即系统的正确性可以由组成它的 IP 的正
确性来保证. 契约描述了一个 IP 的输入与输出之间的逻辑公式. 可以考虑采用统一程序理论 (unifying theories of
programming, UTP) [33] 作为软件 IP 契约 (形式规约) 的表示方法. UTP 的思想是来自于物理学中的大统一理论, 它
的愿景是统一所有风格的编程范式. 在 UTP 中, 变量 x 本身表示该变量的初始值, x'表示该变量的终止值, 那么程
序的行为可以表示成所有 x 和 x'之间的逻辑公式 (谓词关系). 例如, 以下是用 UTP 书写的程序形式规约.

Variable declaration:
● Inputs: u, y: R
● Outputs: x, z: R
Assumptions: y ≠ 0
Guarantees: x' > u ∧ z' = x' / y
该形式规约是一个假设/保证 (assume/guarantee)-契约, 它描述了程序的输入是 u 和 y, 输出是 x 和 z, 它们都是
实数类型. 如果输入 y ≠ 0 (assume), 那么该软件 IP 将保证输出 x' > u 并且 z' = x' / y (guarantee); 反之, 如果输入 y =
0 (违反假设), 那么该软件 IP 将不会有任何保证, 即输出 x 和 z 可以是任意值.
4.2 非功能约束
软件 IP 的非功能约束主要包括运行环境约束、资源约束和性能约束等. 运行环境约束包括对处理器的要求
(处理器版本与主频)、编译器的要求 (编译器版本与编译选项), 以及操作系统的要求 (操作系统版本); 资源约束包
括 IP 占用的内存空间约束; 性能约束包括 IP 在运行时的响应时间和一次执行时间约束. 这些约束可以通过一阶
逻辑公式表示.
4.3 IP 不变式
一个软件 IP 可能包含状态变量 (详见第 5 节), IP 不变式描述了软件 IP 在动态运行过程中状态变量值始终满