aboutsummaryrefslogtreecommitdiffstats
path: root/ajdoc/testdata/figures-demo
diff options
context:
space:
mode:
Diffstat (limited to 'ajdoc/testdata/figures-demo')
-rw-r--r--ajdoc/testdata/figures-demo/.cvsignore1
-rw-r--r--ajdoc/testdata/figures-demo/figures.lst3
-rw-r--r--ajdoc/testdata/figures-demo/figures/Box.java55
-rw-r--r--ajdoc/testdata/figures-demo/figures/Canvas.java11
-rw-r--r--ajdoc/testdata/figures-demo/figures/ColorControl.java20
-rw-r--r--ajdoc/testdata/figures-demo/figures/Enforcement.java65
-rw-r--r--ajdoc/testdata/figures-demo/figures/FigureElement.java21
-rw-r--r--ajdoc/testdata/figures-demo/figures/Group.java88
-rw-r--r--ajdoc/testdata/figures-demo/figures/Line.java73
-rw-r--r--ajdoc/testdata/figures-demo/figures/Log.java34
-rw-r--r--ajdoc/testdata/figures-demo/figures/Point.java59
-rw-r--r--ajdoc/testdata/figures-demo/figures/ShapeFigureElement.java38
-rw-r--r--ajdoc/testdata/figures-demo/figures/SlothfulPoint.java42
13 files changed, 510 insertions, 0 deletions
diff --git a/ajdoc/testdata/figures-demo/.cvsignore b/ajdoc/testdata/figures-demo/.cvsignore
new file mode 100644
index 000000000..ad69a1aa9
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/.cvsignore
@@ -0,0 +1 @@
+figures-demo-all.ajsym
diff --git a/ajdoc/testdata/figures-demo/figures.lst b/ajdoc/testdata/figures-demo/figures.lst
new file mode 100644
index 000000000..9e12310e0
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures.lst
@@ -0,0 +1,3 @@
+figures/*.java
+figures/support/*.java
+figures/gui/*.java
diff --git a/ajdoc/testdata/figures-demo/figures/Box.java b/ajdoc/testdata/figures-demo/figures/Box.java
new file mode 100644
index 000000000..4db7f439d
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Box.java
@@ -0,0 +1,55 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public class Box extends ShapeFigureElement {
+ private Point _p0;
+ private Point _p1;
+ private Point _p2;
+ private Point _p3;
+
+ public Box(int x0, int y0, int width, int height) {
+ _p0 = new Point(x0, y0);
+ _p1 = new Point(x0+width, y0);
+ _p2 = new Point(x0+width, y0+height);
+ _p3 = new Point(x0, y0+height);
+ }
+
+ public Point getP0() { return _p0; }
+ public Point getP1() { return _p1; }
+ public Point getP2() { return _p2; }
+ public Point getP3() { return _p3; }
+
+ public void move(int dx, int dy) {
+ _p0.move(dx, dy);
+ _p1.move(dx, dy);
+ _p2.move(dx, dy);
+ _p3.move(dx, dy);
+ }
+
+ public void checkBoxness() {
+ if ((_p0.getX() == _p3.getX()) &&
+ (_p1.getX() == _p2.getX()) &&
+ (_p0.getY() == _p1.getY()) &&
+ (_p2.getY() == _p3.getY()))
+ return;
+ throw new IllegalStateException("This is not a square.");
+ }
+
+ public String toString() {
+ return "Box(" + _p0 + ", " + _p1 + ", " + _p2 + ", " + _p3 + ")";
+ }
+
+ public Shape getShape() {
+ return new Rectangle(getP1().getX(),
+ getP1().getY(),
+ getP3().getX() - getP1().getX(),
+ getP3().getY() - getP1().getY());
+ }
+}
+
diff --git a/ajdoc/testdata/figures-demo/figures/Canvas.java b/ajdoc/testdata/figures-demo/figures/Canvas.java
new file mode 100644
index 000000000..e5491d7cb
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Canvas.java
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+public class Canvas {
+ public static void updateHistory() {
+ // not implemented
+ }
+}
diff --git a/ajdoc/testdata/figures-demo/figures/ColorControl.java b/ajdoc/testdata/figures-demo/figures/ColorControl.java
new file mode 100644
index 000000000..46d1ba428
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/ColorControl.java
@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.Color;
+import figures.FigureElement;
+
+public aspect ColorControl {
+ public static void setFillColor(FigureElement fe, Color color) {
+ // fill in here
+ }
+
+ public static void setLineColor(FigureElement fe, Color color) {
+ // fill in here
+ }
+
+ // fill in here
+}
diff --git a/ajdoc/testdata/figures-demo/figures/Enforcement.java b/ajdoc/testdata/figures-demo/figures/Enforcement.java
new file mode 100644
index 000000000..95ea2e780
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Enforcement.java
@@ -0,0 +1,65 @@
+/*
+ * (c) Copyright 2001 MyCorporation.
+ * All Rights Reserved.
+ */
+
+package figures;
+
+public aspect Enforcement {
+
+ before(int newValue): set(int Point.*) && args(newValue) {
+ if (newValue < 0) {
+ throw new IllegalArgumentException("> val: " + newValue + " is too small");
+ }
+ }
+
+ declare warning: call(void Canvas.updateHistory(..)) && !within(Enforcement): "";
+
+ after() returning: call(void FigureElement+.set*(..)) {
+ //Canvas.updateHistory();
+ }
+
+ declare error:
+ set(private * FigureElement+.*) &&
+ !(withincode(* FigureElement+.set*(..)) || withincode(FigureElement+.new(..))):
+ "should only assign to fileds from set methods";
+
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+// before(int newValue): set(int Point.*) && args(newValue) {
+// if (newValue < 0) {
+// throw new IllegalArgumentException("> value: " + newValue + " too small");
+// }
+// }
+//
+// declare warning: call(void Canvas.updateHistory(..)) && !within(Enforcement):
+// "found call";
+//
+// after() returning: call(void FigureElement+.set*(..)) {
+// Canvas.updateHistory();
+// }
+//
+// declare error:
+// set(private * FigureElement+.*) &&
+// !(withincode(* FigureElement+.set*(..)) || withincode(FigureElement+.new(..))):
+// "should only assign to fields from set methods";
diff --git a/ajdoc/testdata/figures-demo/figures/FigureElement.java b/ajdoc/testdata/figures-demo/figures/FigureElement.java
new file mode 100644
index 000000000..ae06c132b
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/FigureElement.java
@@ -0,0 +1,21 @@
+/*
+Copyright (c) 2001-2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public interface FigureElement {
+ public static final int MIN_VALUE = 0;
+ public static final int MAX_VALUE = 500;
+
+ public abstract void move(int dx, int dy);
+
+ public abstract Rectangle getBounds();
+
+ public abstract boolean contains(Point2D p);
+
+ public abstract void paint(Graphics2D g2);
+}
diff --git a/ajdoc/testdata/figures-demo/figures/Group.java b/ajdoc/testdata/figures-demo/figures/Group.java
new file mode 100644
index 000000000..59c1a17cf
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Group.java
@@ -0,0 +1,88 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.util.*;
+import java.awt.*;
+import java.awt.geom.*;
+
+public class Group implements FigureElement {
+ private Collection _members;
+ private String _identifier;
+
+ public Group(FigureElement first) {
+ this._members = new ArrayList();
+ add(first);
+ }
+
+ public void add(FigureElement fe) {
+ _members.add(fe);
+ }
+
+ public Iterator members() {
+ return _members.iterator();
+ }
+
+ public void move(int dx, int dy) {
+ for (Iterator i = _members.iterator(); i.hasNext(); ) {
+ FigureElement fe = (FigureElement)i.next();
+ fe.move(dx, dy);
+ }
+ }
+
+ public void resetIdentifier(String identifier) {
+ resetIdentifier(identifier);
+ }
+
+ public String toString() {
+ if (_identifier != null) {
+ return _identifier;
+ }
+
+ StringBuffer buf = new StringBuffer("Group(");
+ for (Iterator i = _members.iterator(); i.hasNext(); ) {
+ buf.append(i.next().toString());
+ if (i.hasNext()) {
+ buf.append(", ");
+ }
+ }
+ buf.append(")");
+ return buf.toString();
+ }
+
+ public Rectangle getBounds() {
+ Rectangle previous = null;
+ for (Iterator i = _members.iterator(); i.hasNext(); ) {
+ FigureElement fe = (FigureElement)i.next();
+ Rectangle rect = fe.getBounds();
+ if (previous != null) {
+ previous = previous.union(rect);
+ } else {
+ previous = rect;
+ }
+ }
+ return previous;
+ }
+
+ public boolean contains(Point2D p) {
+ for (Iterator i = _members.iterator(); i.hasNext(); ) {
+ FigureElement fe = (FigureElement)i.next();
+ if (fe.contains(p)) return true;
+ }
+ return false;
+ }
+
+ public void paint(Graphics2D g2) {
+ for (Iterator i = _members.iterator(); i.hasNext(); ) {
+ FigureElement fe = (FigureElement)i.next();
+ fe.paint(g2);
+ }
+ }
+
+ public int size() {
+ return _members.size();
+ }
+}
+
diff --git a/ajdoc/testdata/figures-demo/figures/Line.java b/ajdoc/testdata/figures-demo/figures/Line.java
new file mode 100644
index 000000000..45324646e
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Line.java
@@ -0,0 +1,73 @@
+/*
+Copyright (c) 2001-2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public class Line extends ShapeFigureElement {
+ private Point _p1;
+ private Point _p2;
+
+ public Line(Point p1, Point p2) {
+ _p1 = p1;
+ _p2 = p2;
+ }
+
+ public Point getP1() {
+ return _p1;
+ }
+
+ public void setP1(Point p1) {
+ _p1 = p1;
+ Canvas.updateHistory();
+ }
+
+ public Point getP2() {
+ return _p2;
+ }
+
+ public void setP2(Point p2) {
+ _p2 = p2;
+ Canvas.updateHistory();
+ }
+
+ public void move(int dx, int dy) {
+ //_x = dx;
+ //_y = dy;
+
+ //_p1.move(dx, dy);
+ //_p2.move(dx, dy);
+ }
+
+ public String toString() {
+ return "Line(" + _p1 + ", " + _p2 + ")";
+ }
+
+ /**
+ * Used to determine if this line {@link contains(Point2D)} a point.
+ */
+ final static int THRESHHOLD = 5;
+
+ /**
+ * Returns <code>true</code> if the point segment distance is less than
+ * {@link THRESHHOLD}.
+ */
+ public boolean contains(Point2D p) {
+ return getLine2D().ptLineDist(p) < THRESHHOLD;
+ }
+
+ private Line2D getLine2D() {
+ return new Line2D.Float((float)getP1().getX(),
+ (float)getP1().getY(),
+ (float)getP2().getX(),
+ (float)getP2().getY());
+ }
+
+ public Shape getShape() {
+ return getLine2D();
+ }
+}
+
diff --git a/ajdoc/testdata/figures-demo/figures/Log.java b/ajdoc/testdata/figures-demo/figures/Log.java
new file mode 100644
index 000000000..ed6e0611d
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Log.java
@@ -0,0 +1,34 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+public class Log {
+ private static StringBuffer data = new StringBuffer();
+
+ public static void traceObject(Object o) {
+ throw new UnsupportedOperationException();
+ }
+
+ public static void log(String s) {
+ data.append(s);
+ data.append(';');
+ }
+
+ public static void logClassName(Class _class) {
+ String name = _class.getName();
+ int dot = name.lastIndexOf('.');
+ if (dot == -1) {
+ log(name);
+ } else {
+ log(name.substring(dot+1, name.length()));
+ }
+ }
+
+ public static String getString() {
+ return data.toString();
+ }
+
+ public static void clear() {
+ data.setLength(0);
+ }
+}
diff --git a/ajdoc/testdata/figures-demo/figures/Point.java b/ajdoc/testdata/figures-demo/figures/Point.java
new file mode 100644
index 000000000..e8783a560
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/Point.java
@@ -0,0 +1,59 @@
+/*
+Copyright (c) 2001-2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public class Point extends ShapeFigureElement {
+ private int _x;
+ private int _y;
+
+ public Point(int x, int y) {
+ _x = x;
+ _y = y;
+ }
+
+ public int getX() {
+ return _x;
+ }
+
+ public void setX(int x) {
+ _x = x;
+ //Canvas.updateHistory();
+ }
+
+ public int getY() {
+ return _y;
+ }
+
+ public void setY(int y) {
+ _y = y;
+ //Canvas.updateHistory();
+ }
+
+ public void move(int dx, int dy) {
+ setX(_x + dx);
+ setY(_y + dy);
+ }
+
+ public String toString() {
+ return "Point(" + _x + ", " + _y + ")";
+ }
+
+ /** The height of displayed {@link Point}s. */
+ private final static int HEIGHT = 10;
+
+ /** The width of displayed {@link Point}s. -- same as {@link HEIGHT}. */
+ private final static int WIDTH = Point.HEIGHT;
+
+ public Shape getShape() {
+ return new Ellipse2D.Float((float)getX()-Point.WIDTH/2,
+ (float)getY()-Point.HEIGHT/2,
+ (float)Point.HEIGHT,
+ (float)Point.WIDTH);
+ }
+}
+
diff --git a/ajdoc/testdata/figures-demo/figures/ShapeFigureElement.java b/ajdoc/testdata/figures-demo/figures/ShapeFigureElement.java
new file mode 100644
index 000000000..29a4a89ad
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/ShapeFigureElement.java
@@ -0,0 +1,38 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public abstract class ShapeFigureElement implements FigureElement {
+ public abstract void move(int dx, int dy);
+
+ public abstract Shape getShape();
+
+ public Rectangle getBounds() {
+ return getShape().getBounds();
+ }
+
+ public boolean contains(Point2D p) {
+ return getShape().contains(p);
+ }
+
+ public Color getLineColor() {
+ return Color.black;
+ }
+
+ public Color getFillColor() {
+ return Color.red;
+ }
+
+ public final void paint(Graphics2D g2) {
+ Shape shape = getShape();
+ g2.setPaint(getFillColor());
+ g2.fill(shape);
+ g2.setPaint(getLineColor());
+ g2.draw(shape);
+ }
+}
diff --git a/ajdoc/testdata/figures-demo/figures/SlothfulPoint.java b/ajdoc/testdata/figures-demo/figures/SlothfulPoint.java
new file mode 100644
index 000000000..35c8fb635
--- /dev/null
+++ b/ajdoc/testdata/figures-demo/figures/SlothfulPoint.java
@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2002 Palo Alto Research Center Incorporated. All Rights Reserved.
+ */
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+/**
+ * This class makes mistakes to be caught by invariant checkers.
+ */
+public class SlothfulPoint extends ShapeFigureElement {
+ private int _x;
+ private int _y;
+
+ public SlothfulPoint(int x, int y) {
+ }
+
+ public void setX(int x) {
+ _x = x;
+ }
+
+ public void setY(int y) {
+ _y = y;
+ }
+
+ public void move(int dx, int dy) {
+ //_x += dx;
+ //_y += dy;
+ }
+
+ public String toString() {
+ return "SlothfulPoint";
+ }
+
+ public Shape getShape() {
+ return new Ellipse2D.Float((float)_x,
+ (float)_y, 1.0f, 1.0f);
+ }
+}
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-23 04:01:29 +0000