Computer Science – Software Engineering
Scientific paper
2005-08-24
15th Workshop on Logic Programming Environments (WLPE05), Sitges (Barcelona), Spain, 2005
Computer Science
Software Engineering
17 pages, 15th Workshop on Logic Programming Environments (WLPE05), Sitges (Barcelona), Spain, 2005
Scientific paper
Formal techniques have been shown to be useful in the development of correct software. But the level of expertise required of practitioners of these techniques prohibits their widespread adoption. Formal techniques need to be tailored to the commercial software developer. Alloy is a lightweight specification language supported by the Alloy Analyzer (AA), a tool based on off-the-shelf SAT technology. The tool allows a user to check interactively whether given properties are consistent or valid with respect to a high-level specification, providing an environment in which the correctness of such a specification may be established. However, Alloy is not particularly suited to expressing program specifications and the feedback provided by AA can be misleading where the specification under analysis or the property being checked contains inconsistencies. In this paper, we address these two shortcomings. Firstly, we present a lightweight language called "Loy", tailored to the specification of object-oriented programs. An encoding of Loy into Alloy is provided so that AA can be used for automated analysis of Loy program specifications. Secondly, we present some "patterns of analysis" that guide a developer through the analysis of a Loy specification in order to establish its correctness before implementation.
Heaven William
Russo Alessandra
No associations
LandOfFree
Enhancing the Alloy Analyzer with Patterns of Analysis does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Enhancing the Alloy Analyzer with Patterns of Analysis, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Enhancing the Alloy Analyzer with Patterns of Analysis will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-268889