|||
这是MIT的Daniel Jackson介绍使用relational algebra来模拟抽象模型的书。书是围绕着他创立的Alloy语言及其开源软件工具而写的,但使用First Order Relational Logic(FORL)的技巧是通用的,而且写得非常引人入胜。Alloy工具的独特之处是使用model checker在维度够小的空间全自动地验证模型或给出反例,比起使用theorem prover要容易很多。这是一本有非常独特视角而且虚实兼济的难得好书。网址见:
http://softwareabstractions.org/
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-11-1 07:33
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社