A System for Incrementally Designing and Verifying Programs, Volume I.

摘要

SID (System for Incremental Development) is a computer system for incrementally designing and verifying large, complex programs. It executes commands, proposes actions, answers questions, and accepts and reasons about new or changed information. SID has three main, distinctive characteristics: (1) it provides several useful incremental capabilities, including the ability to respond to changes by ensuring that the final problem solution is consistent and by keeping intact still-valid work without complete reprocessing; (2) its user interface has the ability to guide the user through the design and verification and to engage in an interactive English dialog about the potential effects of changes; (3) it supports a substantial programming language which includes features for generating run-time checks, stating concurrent processes and shared data, and developing data abstractions. SID has been used to completely design and verify several programs. Volume 2 (appendix) contains a transcript of a session with SID in which a simple message switching network that allows secure, asynchronous message transfer among a fixed number of users in incrementally developed. (Author)