OptionalInt model: deterministic of/empty/isPresent/isEmpty/getAsInt

src/main/java/java/util/OptionalInt.java

@@ -0,0 +1,78 @@
+/*
+ * Copyright (c) 2012, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.util;
+
+/**
+ * JBMC model of java.util.OptionalInt.
+ * A simple value container: either empty or holds an int.
+ */
+public final class OptionalInt {
+    private final boolean isPresent;
+    private final int value;
+
+    private OptionalInt() {
+        this.isPresent = false;
+        this.value = 0;
+    }
+
+    private OptionalInt(int value) {
+        this.isPresent = true;
+        this.value = value;
+    }
+
+    public static OptionalInt empty() {
+        // DIFFBLUE MODEL LIBRARY Deliberately NOT a cached static singleton
+        // (unlike the JDK internals): OptionalInt's javadoc explicitly
+        // disclaims singleton-ness of empty() and forbids == comparison, so
+        // per-call allocation is contract-conformant -- and a static object
+        // field would become nondeterministic under JBMC's --nondet-static,
+        // making empty().isPresent() spuriously satisfiable.
+        return new OptionalInt();
+    }
+
+    public static OptionalInt of(int value) {
+        return new OptionalInt(value);
+    }
+
+    public boolean isPresent() {
+        return isPresent;
+    }
+
+    public boolean isEmpty() {
+        return !isPresent;
+    }
+
+    public int getAsInt() {
+        if (!isPresent) {
+            throw new NoSuchElementException("No value present");
+        }
+        return value;
+    }
+
+    public int orElse(int other) {
+        return isPresent ? value : other;
+    }
+}