Conference
DynAlloy
Abstract
We present DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems using actions. Actions allow us to appropriately specify dynamic properties, particularly, properties regarding execution traces, in the style of dynamic logic specifications.We extend Alloy's syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra's weakest liberal precondition. …
Authors
Frias MF; Galeotti JP; Pombo CGL; Aguirre NM
Pagination
pp. 442-451
Publisher
Association for Computing Machinery (ACM)
Publication Date
2005
DOI
10.1145/1062455.1062535
Name of conference
Proceedings of the 27th international conference on Software engineering - ICSE '05