[ERTS2012] 航天器星载软件形式化模型驱动研发 —— 对 Scade 语言本身的影响

在《从ERTS学习SCADE发展》中提到，在 ERTS 会议中，Scade团队会在该会议中介绍与Scade相关的工作。在 ERTS 2012 中，Scade 团队介绍了使用Scade作为主要工具，应用在航天器星载软件开发中的相关话题。原材料可参考 《Formal Model Driven Engineering for Space Onboard Software》csdn.net。

在 ERTS 2012 上，Scade 团队介绍了 Scade 在星载软件中的应用。内容主题与使用 Scade 建模生成 SPARK 星载软件程序有关。在本篇中，注意力将集中在该工作对 Scade 语言本身的影响方面。

在星载软件项目的推进过程中，Scade 团队使 Scade 6 编译器支持了 SPARK 代码的生成。SPARK 是具备语义形式化定义的Ada子集。在这项工作中，对 Scade 6 本身的语言特性进行了拓展。

新增数值类型

层次化的数值类型

对 Scade 6 拓展了数值类型

int, int8, int16, int32, int64, uint8, uint16, uint32, uint64, integer, 
numeric, real, float32, numeric, floating, float64 

不同的数字类型不兼容，例如，不能将 int8 类型的流和 int32 类型的流相加。对于每个内置类型，都存在一个与类型同名的强制转换运算符：int8、int16、int32 等。

多态运算符的数值约束

与 numeric 一样，integer 和 floating 关键字不能直接参与类型表达式，但它们可用于指定数值约束，以限制用户定义运算符的多态性。

比如例子1

function imported N1 (x:'t) returns (y:'t) where 't numeric;

中，类型变量可以是任何数值类型。

例子2

function imported N2 (x:'t) returns (y:'t) where 't integer ;

可以由 Integer 的任何子类型实例化（在数字类型的层次结构中）。

例子3

function imported N3 (x:'t) returns (y:'t) where 't floating ;

可以由 floating 的任何子类型实例化。

数值类型的类型转换

对 Scade 6 引入了一个通用的强制转换运算符 （<expr>：<type_expr>），用于数字类型（包括内置、导入和多态类型）之间的转换，例如：

type imported Timp is numeric; 

function F (x1: int8 ; x2:'t) 
returns (y1: float32 ; y2:'t; y3: Timp) where 't floating 
let 
    y1 = (x1: float32); -- equivalent to float32 (x1); 
    y2 = (x1:'t); 
    y3 = (x2: Timp); 
tel

所有浮点到整数的强制转换现在都使用 “截断” 语义。在 C 语言中，这已经是默认行为。在生成的 SPARK 代码中，我们在转换浮点值之前使用 'Truncation 属性。

总结

对比 Scade 6 与其他同步数据流语言，Scade 的比较显著的不同之处的一个方面为对数值类型的层次化细分。而从 ERTS 2012 可注意到，该特色的由来源自 Scade 编译器对Ada代码的生成研发所伴生的产物。