[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Victor Kuncak & Patrick Lam & Karen Zee & Martin C Rinard
- Modular Pluggable Analysis for Data Structure Consistency
- IEEE Computer Magazine V39n12(Dec 2006)pp988-1005
- =DEMO TOOL Hob MODULAR PROVING REALITY SETS RELATIONS ABSTRACTION PALE Bohn Isabelle flag ADTs Minesweeper httpd etc
- Shows that the theories of ADTs from the 80s are the basis for a set of tools.
- Modules have three parts: implementation, specification, and abstraction.
- The code inside modules is proved to support certain assertions expressed in the language of set theory. The abstraction section defines higher level formulas using sets and the calculus of relations -- like Alloy.
- Programs are proved using the higher-level properties.
- Page 989. "One somewhat unusual feature of these abstract properties is that are outward looking: the capture important features of the system that are directly meaning ful to the users.
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]