List of All Sidenotes

Concepts and Philosophy

These sidenotes describe important concepts and ideas, and are mostly not Alloy-specific.

  • Pretending Alloy is an OO program (sidenote-OO-paradigm.html)
  • Three levels of understanding/reading an Alloy model (sidenote-levels-of-understanding.html)
  • Operational vs. Declarative modeling (sidenote-operational-declarative.html)
  • Thinking of relations as sets of tuples (sidenote-relations-are-ordered-pairs.html)
  • Everything in Alloy is a relation (or an Atom) (sidenote-relations-everywhere.html)
  • Higher order relations (sidenote-ternary.html)
  • Detecting and eliminating overconstraint (sidenote-overconstraint.html)
  • Detecting and eliminating underconstraint (sidenote-underconstraint.html)
  • What is a function? (sidenote-relation-function.html)

    Syntax and Semantics

    These sidenotes describe syntax and formal definitions, and are mostly Alloy-specific.

  • Combining modules with open (sidenote-combining-modules.html)
  • Attaching an appended fact to a signature (sidenote-format-appended-fact.html)
  • Higher arity function signatures using -> (sidenote-format-arrow.html)
  • Multiplicity markings on relational products: '?' and '!' (sidenote-multiplicity.html)
  • Making claims with assert (sidenote-format-assert.html)
  • verifying claims with check (sidenote-format-check.htmls)
  • Three ways to write a comment (sidenote-format-comments.html)
  • Adding constraints with fact (sidenote-format-fact.html)
  • writing functions with fun (sidenote-format-functions.html)
  • writing predicates with pred (sidenote-format-pred.html)
  • beginnning a model with module (sidenote-format-module.html)
  • viewing examples with run (sidenote-format-run.html)
  • creating sets/classes/signatures with sig (sidenote-format-sig.html)
  • Logical Operations such as ||, &&, =>, <=>, and ! (sidenote-logic-ops.html)
  • non-reflexive transitive closure (.^) (sidenote-nrtc.html)
  • Qualifiers such as set and option (sidenote-qualifiers.html)
  • Quantifiers such as all, some, no, one, and sole (sidenote-quantifiers.html)
  • Relational Operations such as ~ and -> (sidenote-relation-ops.html)
  • Relational Join/Composition (.) (::) (sidenote-relational-join.html)
  • reflexive transitive closure (.*) (sidenote-rtc.html)
  • Set Operations such as +, &, -, and in (sidenote-set-ops.html)

    Supporting Roles

    These sidenotes don't stand on their own.

  • Description of the River Crossing puzzle (sidenote-RC-puzzle.html)
  • Solution to the River Crossing puzzle (sidenote-RC-solution.html)
  • explanation of why the file system must be acyclic (sidenote-acyclic-explanation.html)
  • alternative to defineContents (sidenote-alternative-defineContents.html)
  • Alternative to using part (sidenote-alternative-part.html)
  • Alternative ways to specify scope for run example (sidenote-alternative-run-example.html)
  • Alternative ways to specify scope for run solvePuzzle (sidenote-alternative-run-solvepuzzle.html)
  • Alternative ways to accomplish the effects of static and as appended fact (sidenote-alternative-static-appended.html)
  • Why there can't be more than one item (sidenote-answer-other.html)
  • Summary of the Walkthrough: "Runthrough" (sidenote-runthrough.html)

    Utility

    These sidenotes serve to introduce the tutorial and make it flow better, but don't have much to do with the content of the tutorial.

  • List of all sidenotes (this sidenote) (sidenote-all.html)
  • Alloy/Tutorial contact information (sidenote-contact-info.html)
  • blank sidenote (sidenote-default.html)
  • example sidenote (sidenote-intro.html)

    list all sidenotes

    clear this sidenote