As a start, we give further examples of Alloy specifications. Next we turn to specification of imperative programs. Assertions about programs are specifications of how the program is supposed to behave. Assertions can be used for correctness reasoning and for testing. We illustrate the important notions of preconditions and postconditions. We demonstrate how the state transitions of imperative programming can be modelled as relations in Alloy. Correctness reasoning can be linked to testing and debugging by means of executable assertions, and by means of random generation of test cases based on preconditions and postconditions
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Program Verification, Defeasible Reasoning, and Two Views of Computer Science.Timothy R. Colburn - 1991 - Minds and Machines 1 (1):97-116.
Comparing Contextualism and Invariantism on the Correctness of Contextualist Intuitions.Jessica Brown - 2005 - Grazer Philosophische Studien 69 (1):71-100.
Can It Be Morally Permissible to Assert a Falsehood in Service of a Good Cause?Christopher Kaczor - 2012 - American Catholic Philosophical Quarterly 86 (1):97-109.
On Existence in Set Theory.Rodrigo A. Freire - 2012 - Notre Dame Journal of Formal Logic 53 (4):525-547.
Performatives and Antiperformatives.Ingvar Johansson - 2003 - Linguistics and Philosophy 26 (6):661-702.
Efficiency in Data Gathering: Set Size Effects in the Selection Task.Raymond S. Nickerson & Susan F. Butler - 2008 - Thinking and Reasoning 14 (1):60 – 82.
Added to index2010-11-21
Total downloads17 ( #282,280 of 2,164,237 )
Recent downloads (6 months)1 ( #348,039 of 2,164,237 )
How can I increase my downloads?