User Tools

Site Tools


invariant:intro

Intro Ex1 Ex2 Ex3 Ex4 Ex5

Invariants: Intro

In the following exercises, we will demonstrate the use of AspectJ to check both static and dynamic invariants in the context of a graphical figure editor.

Set-up

  1. Create a new AspectJ Project in Eclipse
  2. Download the source of the figure editor: figures.zip
  3. In Eclipse, select FileImport…. Choose to import files from an Archive File and point to the file you just downloaded.
  4. To resolve the build errors for the included tests, right-click your new project, select Build PathAdd Libraries…. Click JUnit and select version 3.x.

Running the Figure Editor

You can run the figure editor through the class figures.gui.Main. Right-click it and select Run AsAspectJ/Java Application.

Running the Tests

The source archive you downloaded contains a number of test suites. The tests of the suite CoreTest should always pass. You can run them by right-clicking on this class and selecting Run AsJUnit Test.

The other test suites can be used to verify your answers to the following exercises.


Start the Invariants track at Exercise 1.

invariant/intro.txt · Last modified: 2021/02/05 13:53 (external edit)