JPL 的代码规范

好奇号上了火星。那让我们看看喷气推进实验室的代码规范 JPL Institutional Coding Standard

规范强调的是可证明性。比如3和4要求所有循环都有循环上限,并且不允许递归,这是为了静态分析工具能够验证程序的运行时间和空间的上界;而5禁止使用动态分配内存,一是为了避免内存分配时的不确定性,二是为了能够验证程序运行空间的上界。
当然,上面几条规范主要是为了安全关键的软件,常规的软件开发不需要做到这个地步。但是可证明性的思想是非常有意义的。
后面的规范就平易近人多了,模块间只用IPC通信,共享数据的单一所有者,线程安全,尽可能避免锁和嵌套锁;尽可能小的作用域,检查所有输入参数和返回值,必须使用断言;等。

看不了这么多也可以看作为精简版的 The Power of Ten — Rules for Developing Safety Critical Code

好奇号用的是 400MIPS 的 RAD750 抗辐射处理器,256kB EEPROM,256MB DRAM,2GB 闪存,VxWorks 实时操作系统。能源是放射性同位素热电机。

Advertisements
This entry was posted in Computer and Internet, Programming and Algorithm and tagged , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s