liquidjava/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java at 9d3344e46e52c430aade53ef648b1f387d968683 · liquid-java/liquidjava · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
package testBooleanGhost;

import liquidjava.specification.Ghost;
import liquidjava.specification.StateRefinement;

@Ghost("boolean opened")
@Ghost("boolean closed")
public class BooleanGhostClass {

	boolean opened;
	boolean closed;

	@StateRefinement(from = "!opened(this) && !closed(this)", to = "opened(this) && !closed(this)")
	void open() {
		opened = true;
	}

	@StateRefinement(from = "opened(this) && !closed(this)")
	void execute() {
		// System.out.println("opened:" + open + "\nclosed::" + closed); // lança
		// exceção

		System.out.println("opened: ");
		System.out.println(opened);
		System.out.println("\nclosed: ");
		System.out.println(closed);

	}

	@StateRefinement(from = "opened(this) && !closed(this)", to = "opened(this) && closed(this)")
	void close() {
		closed = true;
	}

	@StateRefinement(from = "opened(this) && closed(this)")
	void terminate() {
		System.out.println("Terminating\n");
	}
}