[巴黎高师课程] 同步反应式系统第二课 - 同步数据流语言 Lustre v4, Lustre v6, Scade 6, Heptagon

在2024-2025学期的巴黎高师同步反应式系统(2024-2025)第三课中，详细讨论同步数据流语言 Lustre v4, Lustre v6, Scade 6, Heptagon相关的语言特性。本文将提供对这些同步语言的介绍。对课程的详细内容，可参考同步反应式系统

介绍

课程主要介绍了Lustre语言及其扩展，用于同步反应系统的设计与实现，以及其他语言如Scade 6, Heptagon等。课程中首先概述了Lustre的核心理念，即通过数学方程直接编写程序规范，并对其进行分析、转换、模拟、测试和验证，最终自动生成可执行代码。接下来详细讲解了Lustre中的数组、模块化复位（modular reset）以及状态机的实现方式。对于数组，文章对比了Lustre v4和v6的不同处理方法，强调了现代Lustre数组作为不可变数据结构的特点。模块化复位部分展示了如何简化复位操作，避免全局传递复位信号。状态机部分则介绍了两种预占方式（强预占和弱预占），并通过实例解释了状态机在不同模式下的行为。

参考

• Lustre v4,https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/lv4-html/index.html
• Lustre v6, https://verimag.univ-grenoble-alpes.fr/Lustre-V6.html?lang=en
• Heptagon,https://gitlab.inria.fr/synchrone/heptagon