examples/TestExample.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 class T1 {
  20   int d = 42;
  21
  22   public int func1(int a, int b) {
  23     if (a > b) {
  24       return 1;
  25     } else if (a == b) {
  26       return 0;
  27     } else {
  28       return -1;
  29     }
  30   }
  31
  32   public boolean func2(boolean cond) {
  33     if (cond && (d > 40)) {
  34       d--;
  35     } else {
  36       d++;
  37     }
  38     return cond;
  39   }
  40 }
  41
  42 class T2 {
  43
  44   public int computeSomething (int a, int b){
  45     try {
  46       return a / b;
  47     } catch (ArithmeticException ax){
  48       return -1; // pretty lame error handling
  49     }
  50   }
  51
  52   public void doSomething() {
  53     System.out.println("something");
  54   }
  55 }
  56
  57 public class TestExample {
  58
  59   public static void main(String[] args) {
  60     T1 t1 = new T1();
  61
  62     assert t1.func1(1, 0) > 0;
  63     assert t1.func1(0, 1) < 0;
  64
  65     assert t1.func2(true) == true;
  66     assert t1.func2(false) == false;
  67
  68
  69     T2 t2 = new T2();
  70
  71     assert t2.computeSomething(42, 42) == 1.0;
  72   }
  73 }
  74