122:
161:, the Alloy Analyzer performs model-finding over restricted scopes consisting of a user-defined finite number of objects. This has the effect of limiting the generality of the results produced by the Analyzer. However, the designers of the Alloy Analyzer justify the decision to work within limited scopes through an appeal to the
144:
Through version 3.0, the Alloy
Analyzer incorporated an integral SAT-based model-finder based on an off-the-shelf SAT-solver. However, as of version 4.0 the Analyzer makes use of the Kodkod model-finder, for which the Analyzer acts as a front-end. Both model-finders essentially translate a model
153:
formula, and then invoke an off-the-shelf SAT-solver on the boolean formula. In the event that the solver finds a solution, the result is translated back into a corresponding binding of constants to variables in the relational logic model.
137:. However, model-checking is ill-suited to the kind of models that are typically developed in Alloy, and as a result the core of the Analyzer was eventually implemented as a model-finder built atop a
462:
129:
The Alloy
Analyzer was specifically developed to support so-called "lightweight formal methods". As such, it is intended to provide fully automated analysis, in contrast to the
467:
133:
techniques commonly used with specification languages similar to Alloy. Development of the
Analyzer was originally inspired by the automated analysis provided by
437:
472:
310:
63:
55:
in that it permits the definition of infinite models. The Alloy
Analyzer is designed to perform finite scope checks even on infinite models.
294:
59:
356:
457:
91:
138:
45:
452:
51:
Although Alloy is designed with automatic analysis in mind, Alloy differs from many specification languages designed for
392:
Andoni, Alexandr; Daniliuc, Dumitru; Khurshid, Sarfraz; Marinov, Darko (2002). "Evaluating the small scope hypothesis".
110:
165:: that a high proportion of bugs can be found by testing a program for all test inputs within some small scope.
426:
431:
393:
326:
29:
272:
Because Alloy is a declarative language the meaning of a model is unaffected by the order of statements.
158:
21:
477:
398:
173:
Alloy models are relational in nature, and are composed of several different kinds of statements:
83:
121:
306:
37:
146:
17:
367:
130:
33:
52:
446:
421:
150:
134:
67:
352:
79:
78:
The first version of the Alloy language appeared in 1997. It was a rather limited
102:
101:
The mathematical underpinnings of the language were heavily influenced by the
302:
95:
330:
256:
are parameterized constraints, and can be used to represent operations
106:
120:
87:
48:. Alloy specifications can be checked using the Alloy Analyzer.
32:
for expressing complex structural constraints and behavior in a
58:
The Alloy language and analyzer are developed by a team led by
36:. Alloy provides a simple structural modeling tool based on
416:
225:- this establishes the existence of a relation between
82:
language. Succeeding iterations of the language "added
180:
define the vocabulary of a model by creating new sets
299:
157:In order to ensure the model-finding problem is
250:are constraints that are assumed to always hold
463:Massachusetts Institute of Technology software
8:
44:that can then be automatically checked for
397:
237:is associated with no more than one head
109:of Alloy owes more to languages such as
289:
287:
285:
281:
40:. Alloy is targeted at the creation of
468:Computer-related introductions in 1997
64:Massachusetts Institute of Technology
7:
262:are expressions that return results
366:. Portland, Oregon. Archived from
14:
268:are assumptions about the model
473:Formal specification languages
432:Kodkod analysis engine website
1:
438:An Alloy Metamodel in Ecore
355:; Dennis, G. (April 2008).
131:interactive theorem proving
494:
111:Object Constraint Language
364:First ACM Alloy Workshop
357:"Kodkod for Alloy Users"
458:Satisfiability problems
422:Alloy Github Repository
213:that contains a field
163:small scope hypothesis
126:
74:History and influences
30:specification language
149:into a corresponding
124:
453:Formal methods tools
209:defines a signature
193:defines a signature
22:software engineering
98:, and signatures".
233:s such that every
203:List{ head :
139:boolean SAT solver
127:
117:The Alloy Analyzer
312:978-0-262-10114-1
221:and multiplicity
38:first-order logic
28:is a declarative
485:
404:
403:
401:
389:
383:
382:
380:
378:
372:
361:
349:
343:
342:
340:
338:
329:. Archived from
323:
317:
316:
291:
208:
192:
147:relational logic
18:computer science
493:
492:
488:
487:
486:
484:
483:
482:
443:
442:
413:
408:
407:
391:
390:
386:
376:
374:
373:on 22 June 2010
370:
359:
351:
350:
346:
336:
334:
325:
324:
320:
313:
295:Jackson, Daniel
293:
292:
283:
278:
199:
187:
171:
169:Model structure
125:Alloy Analyzer.
119:
80:object modeling
76:
34:software system
12:
11:
5:
491:
489:
481:
480:
475:
470:
465:
460:
455:
445:
444:
441:
440:
435:
429:
427:Guide to Alloy
424:
419:
412:
411:External links
409:
406:
405:
384:
344:
333:on 7 June 2007
318:
311:
280:
279:
277:
274:
270:
269:
263:
257:
251:
244:
243:
242:
241:
197:
182:
181:
170:
167:
135:model checkers
118:
115:
75:
72:
60:Daniel Jackson
53:model-checking
13:
10:
9:
6:
4:
3:
2:
490:
479:
476:
474:
471:
469:
466:
464:
461:
459:
456:
454:
451:
450:
448:
439:
436:
433:
430:
428:
425:
423:
420:
418:
417:Alloy website
415:
414:
410:
400:
399:10.1.1.8.7702
395:
388:
385:
369:
365:
358:
354:
348:
345:
332:
328:
322:
319:
314:
308:
304:
300:
296:
290:
288:
286:
282:
275:
273:
267:
264:
261:
258:
255:
252:
249:
246:
245:
240:
236:
232:
228:
224:
220:
216:
212:
206:
202:
198:
196:
190:
186:
185:
184:
183:
179:
176:
175:
174:
168:
166:
164:
160:
155:
152:
151:boolean logic
148:
145:expressed in
142:
140:
136:
132:
123:
116:
114:
112:
108:
104:
99:
97:
93:
89:
85:
81:
73:
71:
69:
68:United States
65:
61:
56:
54:
49:
47:
43:
39:
35:
31:
27:
23:
19:
387:
375:. Retrieved
368:the original
363:
347:
335:. Retrieved
331:the original
321:
298:
271:
265:
259:
253:
247:
238:
234:
230:
226:
222:
218:
214:
210:
204:
200:
194:
188:
177:
172:
162:
156:
143:
128:
100:
92:polymorphism
77:
57:
50:
42:micro-models
41:
25:
15:
327:"Alloy FAQ"
90:relations,
84:quantifiers
46:correctness
478:Z notation
447:Categories
353:Torlak, E.
276:References
266:Assertions
254:Predicates
178:Signatures
105:, and the
103:Z notation
394:CiteSeerX
303:MIT Press
260:Functions
159:decidable
96:subtyping
86:, higher
377:19 April
297:(2006).
217:of type
191:Object{}
337:7 March
66:in the
62:at the
434:at MIT
396:
309:
229:s and
207:Node }
195:Object
107:syntax
371:(PDF)
360:(PDF)
248:Facts
88:arity
26:Alloy
379:2009
339:2013
307:ISBN
239:Node
235:List
231:Node
227:List
223:lone
219:Node
215:head
211:List
205:lone
20:and
201:sig
189:sig
16:In
449::
362:.
305:.
301:.
284:^
141:.
113:.
94:,
70:.
24:,
402:.
381:.
341:.
315:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
