SCADE One vs Scade 6 - 标量积建模比较
在基于模型的设计(Model-Based Design)中,SCADE一直以其形式化建模能力和代码生成的可靠性广受关注。随着SCADE One的推出,语言层面也引入了一些新的特性,其中值得一提的就是forward。
这里通过一个经典的例子——标量积(Scalar Product),来比较SCADE Suite 6与SCADE One在建模风格上的差异,并讨论forward特性带来的优势。
SCADE Suite 6的建模方式:map + fold
在SCADE Suite 6中,常用的写法是借助高阶函数算符map与fold:
-- SCADE Suite/Scade 6
function ScalProd <<n>> (u, v: 'T^n)
returns (w:'T) where 'T numericw = (fold $+$ <<n>>) (0, (map $*$ <<n>>)(u, v));
-
map $*$ <<n>>)(u, v)
将两个向量逐元素相乘,结果是一个长度为n
的列表[u1*v1, u2*v2, …, un*vn]
。 -
(fold $+$ <<n>>) (0, ...)
从初始值0开始,对列表中的元素进行逐一累加,最终得到标量积。
这种风格与是函数式编程风格:通过map描述元素级计算,再用fold汇聚结果。表达简洁,但对于刚接触SCADE的工程师来说,往往需要先理解map/fold语义,才能读懂其中的计算过程。
SCADE One 的建模方式:forward
在SCADE One/Swan中,同样的标量积可以用forward来描述:
-- SCADE One/Swan
function ScalProd <<N>> (u: 'T^N; v: 'T^N)
returns (w: 'T) where 'T numeric
{let w = forward <<N>> with [ui] = u; [vi] = v; let ret = last 'ret + ui * vi;returns (ret : last = 0);
}
这里需要注意forward的使用:
forward <<N>> with [ui] = u; [vi] = v;
相当于一个隐式的 for 循环,在一次计算周期内依次遍历 u 和 v 的元素。let ret = last 'ret + ui * vi;
在迭代过程中,ret累积结果,last 提供上一次迭代的值(初始值 0)。
换句话说,这段代码如同通用程序语言里的:
ret = 0
for i in range(N):ret = ret + u[i] * v[i]
表达方式比map+fold
更贴近工程师熟悉的迭代逻辑。虽然forward仍然是单周期完成所有迭代,但在语义上显得更直观。
map+fold
解法与forward
解法比较
forward
提供了类for-loop语义。在map+fold
中,需要“抽象地”思考:先把整个乘积列表算出来,再折叠。在forward中,直接写出逐步累积的过程,接近工程师在C/Python中实现标量积的方式。
同时减少了嵌套抽象。map与fold的组合,需要工程师对函数式算符有较强的掌握。forward将迭代逻辑直接表达在语句里,避免了抽象算符的嵌套。
使用forward也有更好的可扩展性。如果在标量积的基础上增加逻辑(如:条件判断、过滤部分元素),在map+fold下会变得繁琐,而在forward下,只需在迭代体中加入条件即可(until/unless)。
使用方式也符合熟悉Matlab控制系统工程师的思维,forward提供了一种与常规编程更一致的建模方式,降低了建模心智负担。