Adding new examples and tests: Groovy and Java programs.

[jpf-core.git] / examples / TestExample.java

diff --git a/examples/TestExample.java b/examples/TestExample.java
new file mode 100644 (file)
index 0000000..48aebdc
--- /dev/null
+++ b/examples/TestExample.java
@@ -0,0 +1,74 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+class T1 {
+  int d = 42;
+
+  public int func1(int a, int b) {
+    if (a > b) {
+      return 1;
+    } else if (a == b) {
+      return 0;
+    } else {
+      return -1;
+    }
+  }
+
+  public boolean func2(boolean cond) {
+    if (cond && (d > 40)) {
+      d--;
+    } else {
+      d++;
+    }
+    return cond;
+  }
+}
+
+class T2 {
+
+  public int computeSomething (int a, int b){
+    try {
+      return a / b;
+    } catch (ArithmeticException ax){
+      return -1; // pretty lame error handling
+    }
+  }
+
+  public void doSomething() {
+    System.out.println("something");
+  }
+}
+
+public class TestExample {
+
+  public static void main(String[] args) {
+    T1 t1 = new T1();
+
+    assert t1.func1(1, 0) > 0;
+    assert t1.func1(0, 1) < 0;
+
+    assert t1.func2(true) == true;
+    assert t1.func2(false) == false;
+
+
+    T2 t2 = new T2();
+
+    assert t2.computeSomething(42, 42) == 1.0;
+  }
+}
+