BigInteger now as an example

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/Example.java

@@ -31,10 +31,23 @@ public abstract class Example {
         File examplefolder = new File(psdbg.getPath(), FilenameUtils.removeExtension(filename));
 
         File f = new File(examplefolder, filename);
+
         FileUtils.copyURLToFile(url, f);
         return f;
     }
 
+    public static File newTempFile(File file, String filename) throws IOException {
+
+
+        File psdbg = new File(FileUtils.getTempDirectoryPath(), "psdbg");
+        File examplefolder = new File(psdbg.getPath(), FilenameUtils.removeExtension(filename));
+
+        File f = new File(examplefolder, file.getName());
+
+        FileUtils.copyFile(file, f);
+        return f;
+    }
+
     protected void defaultInit(Class aClass) {
         setHelpText(aClass.getResource("help.html"));
         setKeyFile(aClass.getResource("problem.key"));

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java

@@ -11,6 +11,13 @@ import org.apache.commons.io.IOUtils;
 import java.io.*;
 import java.net.URL;
 import java.nio.charset.Charset;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 /**
  * @author Alexander Weigl
@@ -26,6 +33,9 @@ public class JavaExample extends Example {
     @Setter
     private URL projectFile;
 
+    @Getter
+    @Setter
+    private Path directoryPath;
     @Override
     public void open(DebuggerMain debuggerMain) {
         //TODO should be reworked if we have an example
@@ -40,6 +50,23 @@ public class JavaExample extends Example {
             File java = newTempFile(javaFile, getName() + ".java");
             //System.out.println(java.getAbsolutePath());
             //debuggerMain.openKeyFile(key);
+            if(directoryPath != null){
+                try (Stream<Path> paths = Files.walk(directoryPath)) {
+                    List<Path> collect = paths.filter(Files::isRegularFile).collect(Collectors.toList());
+                    List<String> files = new LinkedList<>();
+                    collect.forEach(path -> {
+                        File f = path.toFile();
+                        if(f.getName().endsWith(".java") && !f.getName().equals(getName()+".java")){
+                            try {
+                                File temp = newTempFile(f, getName()+".java");
+
+                            } catch (IOException e) {
+                                e.printStackTrace();
+                            }
+                        }});
+                    files.forEach(path -> System.out.println("path = " + path));
+                }
+            }
             debuggerMain.openJavaFile(java);
             if (settingsFile != null) {
                 File settings = newTempFile(settingsFile, getName() + ".props");

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/bigInteger/BigIntegerExample.java

+package edu.kit.iti.formal.psdbg.examples.java.bigInteger;
+
+import edu.kit.iti.formal.psdbg.examples.JavaExample;
+
+import java.net.URISyntaxException;
+import java.nio.file.Paths;
+
+
+public class BigIntegerExample extends JavaExample {
+
+    public BigIntegerExample() throws URISyntaxException {
+        setName("BigInteger Example");
+
+        setDirectoryPath(Paths.get(getClass().getResource("BigInteger.java").toURI()).getParent());
+        setJavaFile(getClass().getResource("BigInteger.java"));
+        setScriptFile(getClass().getResource("script.kps"));
+
+       // setSettingsFile(getClass().getResource("proof-settings.props"));
+       // setHelpText(getClass().getResource("help.html"));
+
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/RuleCompleter.java

@@ -14,7 +14,7 @@ import java.util.stream.Stream;
  */
 public class RuleCompleter implements AutoCompleter {
     @Getter
-    @Setter
+
     private KeYEnvironment environment;
     private List<Suggestion> suggestions = new ArrayList<>(2048);
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java

@@ -102,7 +102,6 @@ public class ContractChooser extends Dialog<Contract> {
         private void render() {
             if (getItem() != null) {
                 text.getChildren().clear();
-                System.out.println(getItem().getName());
                 String content = content = getItem().getPlainText(services);
 
                 Text contract = new Text("Contract for method: ");

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/AbstractTreeNode.java

@@ -15,7 +15,7 @@ public class AbstractTreeNode {
     @Getter @Setter
     private List<AbstractTreeNode> children;
 
-    @Getter @Setter
+    @Getter
     private final Node node;
 
     @Getter @Setter

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/ForeachTreeNode.java

@@ -21,7 +21,7 @@ public class ForeachTreeNode extends AbstractTreeNode {
     @Getter
     private final PTreeNode<KeyData> scriptState;
 
-    @Getter @Setter
+    @Getter
     private final int linenr;
 
     private final boolean foreachstart;

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/RepeatTreeNode.java

@@ -21,7 +21,7 @@ public class RepeatTreeNode extends AbstractTreeNode {
     @Getter
     private final PTreeNode<KeyData> scriptState;
 
-    @Getter @Setter
+    @Getter
     private final int linenr;
 
     private final boolean repeatstart;

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/ScriptTreeNode.java

@@ -18,7 +18,7 @@ public class ScriptTreeNode extends AbstractTreeNode {
     @Getter
     private final PTreeNode<KeyData> scriptState;
 
-    @Getter @Setter
+    @Getter
     private final int linenr;
 
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeTransformation.java

@@ -14,10 +14,8 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.ProofTreeManager;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import javafx.scene.control.TreeItem;
 import javafx.util.Pair;
-import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import lombok.val;
-import sun.reflect.generics.tree.Tree;
 
 import java.util.*;
 

ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example

@@ -9,6 +9,7 @@ edu.kit.iti.formal.psdbg.examples.java.maxtriplet.MaxTripletExample
 edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort
 edu.kit.iti.formal.psdbg.examples.java.sumPositive.SumPositiveExample
 edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
+edu.kit.iti.formal.psdbg.examples.java.bigInteger.BigIntegerExample
 #edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
 #edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample
 #edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList

ui/src/main/resources/edu.kit.iti.formal.psdbg.examples.java.bigInteger/Arrays.java

+package java.util;
+
+public class Arrays {
+
+}

ui/src/main/resources/edu.kit.iti.formal.psdbg.examples.java.bigInteger/BigInteger.java

+package java.math;
+
+import java.util.Arrays;
+
+public class BigInteger extends Number implements Comparable/*<BigInteger>*/ {
+    /**
+     * The signum of this BigInteger: -1 for negative, 0 for zero, or
+     * 1 for positive.  Note that the BigInteger zero <i>must</i> have
+     * a signum of 0.  This is necessary to ensures that there is exactly one
+     * representation for each BigInteger value.
+     *
+     * @serial
+     */
+    final int signum;
+
+    /**
+     * The magnitude of this BigInteger, in <i>big-endian</i> order: the
+     * zeroth element of this array is the most-significant int of the
+     * magnitude.  The magnitude must be "minimal" in that the most-significant
+     * int ({@code mag[0]}) must be non-zero.  This is necessary to
+     * ensure that there is exactly one representation for each BigInteger
+     * value.  Note that this implies that the BigInteger zero has a
+     * zero-length mag array.
+     */
+    final int[] mag;
+
+    /**
+     * This constant limits {@code mag.length} of BigIntegers to the supported
+     * range.
+     */
+    private static final int MAX_MAG_LENGTH = Integer.MAX_VALUE / Integer.SIZE + 1; // (1 << 26)
+
+    /**
+     * This mask is used to obtain the value of an int as if it were unsigned.
+     */
+    final static long LONG_MASK = 0xffffffffL;
+
+    /**
+     * The BigInteger constant zero.
+     *
+     * @since   1.2
+     */
+    public static final BigInteger ZERO = new BigInteger(new int[0], 0);
+
+
+    /*@ helper normal_behavior
+      @ ensures this.mag == magnitude;
+      @*/
+    BigInteger(int[] magnitude, int signum) {
+
+    }
+
+
+
+
+
+}

ui/src/main/resources/edu.kit.iti.formal.psdbg.examples.java.bigInteger/Comparable.java

+package java.lang;
+import java.util.*;
+
+public interface Comparable/*<T>*/ {
+    public int compareTo(/*T*/ Object o);
+}

ui/src/main/resources/edu.kit.iti.formal.psdbg.examples.java.bigInteger/Math.java

+package java.lang;
+
+public final class Math {
+    public static int min(int a, int b) {
+        return (a <= b) ? a : b;
+    }
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/bigInteger/Arrays.java

+package java.util;
+
+public class Arrays {
+    /*@ public normal_behavior
+      @ requires 0 <= from && from <= original.length && from <= to && original != null;
+      @ ensures \result != original;                                    // always returns a new array
+      @ ensures \result.length == to - from;
+      @ ensures (to <= original.length)
+      @      ==> (\forall int i; from <= i && i < to; \result[i - from] == original[i]);
+      @ ensures (to > original.length)
+      @      ==> ((\forall int i; from <= i && i < original.length; \result[i - from] == original[i])
+      @          && (\forall int i; original.length <= i && i < to; \result[i - from] == 0));
+      @ assignable \nothing;
+      @
+      @ also
+      @
+      @ public exceptional_behavior
+      @ requires from < 0 || from > original.length || from > to || original == null;
+      @ signals (IllegalArgumentException e) from > to;
+      @ signals (ArrayIndexOutOfBoundsException e) from < 0 || from > original.length;
+      @ signals (NullPointerException e) original == null;
+      @ signals_only IllegalArgumentException, ArrayIndexOutOfBoundsException, NullPointerException;
+      @ assignable \nothing;
+      @*/
+    public static int[] copyOfRange(int[] original, int from, int to) {
+        int newLength = to - from;
+        if (newLength < 0)
+            throw new IllegalArgumentException(from + " > " + to);
+        int[] copy = new int[newLength];
+        System.arraycopy(original, from, copy, 0,
+                         Math.min(original.length - from, newLength));
+        return copy;
+    }
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/bigInteger/BigInteger.java

+package java.math;
+
+import java.util.Arrays;
+
+public class BigInteger extends Number implements Comparable/*<BigInteger>*/ {
+    /**
+     * The signum of this BigInteger: -1 for negative, 0 for zero, or
+     * 1 for positive.  Note that the BigInteger zero <i>must</i> have
+     * a signum of 0.  This is necessary to ensures that there is exactly one
+     * representation for each BigInteger value.
+     *
+     * @serial
+     */
+    final int signum;
+
+    /**
+     * The magnitude of this BigInteger, in <i>big-endian</i> order: the
+     * zeroth element of this array is the most-significant int of the
+     * magnitude.  The magnitude must be "minimal" in that the most-significant
+     * int ({@code mag[0]}) must be non-zero.  This is necessary to
+     * ensure that there is exactly one representation for each BigInteger
+     * value.  Note that this implies that the BigInteger zero has a
+     * zero-length mag array.
+     */
+    final int[] mag;
+
+    //@ static invariant BigInteger.ZERO.<inv>;
+    //@ static invariant BigInteger.ZERO.value == 0;
+
+    //@ ghost \bigint value = 0;
+
+    /*@ invariant value == calcValue(signum, mag);
+      @ invariant signum == 0 || signum == 1 || signum == -1;
+      @ invariant signum == 0 <==> mag.length == 0;
+      @ invariant mag.length > 0 ==> mag[0] != 0;
+      @ accessible \inv: signum, mag, mag[*], value;
+      @*/
+
+    // no valid invariant (after RuntimeException inv. has to hold)
+    /*@ invariant mag.length < MAX_MAG_LENGTH || mag.length == MAX_MAG_LENGTH && mag[0] >= 0;
+    */
+
+    // returns the value of the input integer as if it was unsigned
+    /*@ model_behavior
+      @ ensures value == 0 ==> \result == 0;
+      @ ensures value != 0 ==> \result > 0;
+      @ ensures value > 0 ==> \result == value;
+      @ ensures value < 0 ==> \result == value + 0x100000000L;
+      @ ensures \result >= 0;
+      @ ensures \result < 0x100000000L;
+      @ ensures (\forall int i; value != i ==> \result != toUnsigned(i));    // injective function
+      @ accessible \nothing;
+      @ static helper model long toUnsigned(int value) {
+      @     return (long)value & 0xffffffffL;
+      @ }
+      @*/
+
+    // returns 2^(32*exp) = (2^(32))^exp
+    /*@ model_behavior
+      @ requires exp >= 0;
+      @ ensures \result >= 1;
+      @ ensures (\forall int i; 0 <= i && i < exp; twopower(i) < \result);   // strictly increasing
+      @ measured_by exp;
+      @ accessible \nothing;
+      @ static helper model \bigint twopower(int exp) {
+      @     return exp == 0 ? 1 : twopower(exp - 1) * 0x100000000L;
+      @ }
+      @*/
+ 
+    // returns the value of the BigInteger as \bigint
+    /*@ model_behavior
+      @ requires m.length > 0 ==> m[0] != 0;
+      @ requires s == 0 <==> m.length == 0;
+      @ ensures \result
+      @         == s*(\sum int i; 0 <= i && i < m.length; toUnsigned(m[i]) * twopower(m.length-i-1));
+      @ ensures s < 0 ==> \result < 0;
+      @ ensures s == 0 ==> \result == 0;
+      @ ensures s > 0 ==> \result > 0;
+      @ accessible m[*];    // m.length is a function in KeY, not a field, and thus not included here
+      @ static helper model \bigint calcValue(int s, int[] m) {
+      @     return s*(\sum int i; 0 <= i && i < m.length; toUnsigned(m[i]) * twopower(m.length-i-1));
+      @ }
+      @*/
+
+    /**
+     * This constant limits {@code mag.length} of BigIntegers to the supported
+     * range.
+     */
+    private static final int MAX_MAG_LENGTH = Integer.MAX_VALUE / Integer.SIZE + 1; // (1 << 26)
+
+    /**
+     * This mask is used to obtain the value of an int as if it were unsigned.
+     */
+    final static long LONG_MASK = 0xffffffffL;
+
+    /**
+     * The BigInteger constant zero.
+     *
+     * @since   1.2
+     */
+    public static final BigInteger ZERO = new BigInteger(new int[0], 0);
+
+    /**
+     * This internal constructor differs from its public cousin
+     * with the arguments reversed in two ways: it assumes that its
+     * arguments are correct, and it doesn't copy the magnitude array.
+     */
+    /*@ helper normal_behavior 
+      @ requires (   magnitude.length < MAX_MAG_LENGTH
+      @           || magnitude.length == MAX_MAG_LENGTH && magnitude[0] >= 0)
+      @          && (signum == 0 || signum == 1 || signum == -1)
+      @          && (magnitude.length > 0 ==> magnitude[0] != 0)
+      @          && (signum == 0 ==> magnitude.length == 0)
+      @			 && magnitude != null;
+      @	ensures \invariant_for(this);
+      @ ensures this.mag == magnitude;
+      @ ensures (magnitude.length == 0 ==> this.signum == 0) &&
+      @         (magnitude.length != 0 ==> this.signum == signum);
+      @ assignable \nothing;                                // special purity rules for constructors
+      @
+      @ also
+      @
+      @ exceptional_behavior
+      @	requires magnitude != null;
+      @ requires     magnitude.length > MAX_MAG_LENGTH
+      @           || magnitude.length == MAX_MAG_LENGTH && magnitude[0] < 0;
+      @ signals_only ArithmeticException;
+      @ signals (ArithmeticException e) magnitude.length > MAX_MAG_LENGTH
+      @                              || magnitude.length == MAX_MAG_LENGTH && magnitude[0] < 0;
+      @ assignable \nothing;                                // special purity rules for constructors
+      @*/
+    BigInteger(int[] magnitude, int signum) {
+        this.signum = (magnitude.length == 0 ? 0 : signum);
+        this.mag = magnitude;
+        if (mag.length >= MAX_MAG_LENGTH) {
+            checkRange();
+        }
+        /*@ set value = calcValue(this.signum, this.mag); @*/
+    }
+    
+    /**
+     * Returns a BigInteger whose value is {@code (-this)}.
+     *
+     * @return {@code -this}
+     */
+    /*@public normal_behavior
+      @ requires \static_invariant_for(BigInteger);
+      @ ensures \result.value == (-1) * value;
+      @ ensures \invariant_for(result);
+      @assignable \nothing;
+      @*/
+    public BigInteger negate() {
+        return new BigInteger(this.mag, -this.signum);
+    }
+    
+    /**
+     * Returns a BigInteger whose value is the absolute value of this
+     * BigInteger.
+     *
+     * @return {@code abs(this)}
+     */
+    /*@public normal_behavior
+      @ requires \static_invariant_for(BigInteger);
+      @ ensures (value < 0) ==> (\result.value == (-1) * value);
+      @ ensures (value >= 0) ==> (\result.value == value);
+      @ ensures \invariant_for(result);
+      @assignable \nothing;
+      @*/
+    public BigInteger abs() {
+        return (signum >= 0 ? this : this.negate());
+    }
+
+    /**
+     * Returns a BigInteger whose value is {@code (this + val)}.
+     *
+     * @param  val value to be added to this BigInteger.
+     * @return {@code this + val}
+     */
+    /*@ public normal_behavior
+      @ requires val.<inv> && \static_invariant_for(BigInteger);
+      @ requires val.mag.length < MAX_MAG_LENGTH
+      @       || val.mag.length == MAX_MAG_LENGTH && val.mag[0] >= 0;
+      @ requires this.mag.length < MAX_MAG_LENGTH
+      @       || this.mag.length == MAX_MAG_LENGTH && this.mag[0] >= 0;
+      @ ensures \result.value == val.value + this.value;
+      @ ensures \result.<inv>;
+      @ assignable \nothing;
+      @*/
+    public BigInteger add(BigInteger val) {
+        if (val.signum == 0)
+            return this;
+        if (signum == 0)
+            return val;
+        if (val.signum == signum)
+            return new BigInteger(add(mag, val.mag), signum);
+
+        int cmp = compareMagnitude(val);
+        if (cmp == 0)
+            return ZERO;
+        int[] resultMag = (cmp > 0 ? subtract(mag, val.mag)
+                           : subtract(val.mag, mag));
+        resultMag = trustedStripLeadingZeroInts(resultMag);
+
+        return new BigInteger(resultMag, cmp == signum ? 1 : -1);
+    }
+
+    /**
+     * Adds the contents of the int arrays x and y. This method allocates
+     * a new int array to hold the answer and returns a reference to that
+     * array.
+     */
+    /*@ private normal_behavior
+      @ requires \static_invariant_for(BigInteger);
+      @ ensures simpleSum(\result) == simpleSum(x) + simpleSum(y);
+      @ ensures \result.length <= (x.length > y.length ? x.length : y.length) + 1;
+      @ assignable \nothing;
+      @*/
+    private static /*@ helper @*/ int[] add(int[] x, int[] y) {
+        // If x is shorter, swap the two arrays
+        if (x.length < y.length) {
+            int[] tmp = x;
+            x = y;
+            y = tmp;
+        }
+
+        int xIndex = x.length;
+        int yIndex = y.length;
+        int result[] = new int[xIndex];
+        long sum = 0;
+        if (yIndex == 1) {
+            sum = (x[--xIndex] & LONG_MASK) + (y[0] & LONG_MASK) ;
+            result[xIndex] = (int)sum;
+        } else {
+            // Add common parts of both numbers
+        	/*@ loop_invariant 0 <= yIndex && yIndex <= y.length
+            @             && 0 <= xIndex && xIndex <= x.length
+            @             && x.length - xIndex == y.length - yIndex
+            @             && partialSum(result, xIndex)
+            @                + (sum>>>32)*twopower(x.length-xIndex) // borrow from next digit
+            @               == partialSum(x, xIndex)
+            @                + partialSum(y, yIndex);
+            @ assignable result[(result.length-y.length)..(result.length-1)];
+            @ decreases yIndex;
+            @*/
+            while (yIndex > 0) {
+            	
+            	/*@ ensures result[xIndex - 1] == ((toUnsigned(x[xIndex - 1])
+            	@ 	+ toUnsigned(y[yIndex - 1]) + (sum / twopower(1)))) % twopower(1);		 
+            	@ assignable result[xIndex - 1];
+            	@*/
+            	{
+                sum = (x[--xIndex] & LONG_MASK) +
+                      (y[--yIndex] & LONG_MASK) + (sum >>> 32);
+                result[xIndex] = (int)sum;
+            	}
+            }
+        }
+        // Copy remainder of longer number while carry propagation is required
+        boolean carry = (sum >>> 32 != 0);
+        /*@ loop_invariant 0 <= xIndex && xIndex <= x.length
+        @                && partialSum(result, xIndex)
+        @                 == partialSum(x, xIndex) + partialSum(y, 0)
+        @                    + (carry ? twopower(x.length-xIndex) : (\bigint)0);
+        @ assignable result[*];
+        @ decreases xIndex;
+        @*/
+        while (xIndex > 0 && carry)
+            carry = ((result[--xIndex] = x[xIndex] + 1) == 0);
+
+        /*@ loop_invariant xIndex >= 0
+        @             && partialSum(result, xIndex) == partialSum(x, xIndex)
+        @                                              + partialSum(y, 0);
+        @ assignable result[*];
+        @ decreases xIndex;
+        @*/
+        while (xIndex > 0)
+            result[--xIndex] = x[xIndex];
+
+        // Grow result if necessary
+        if (carry) {
+            int bigger[] = new int[result.length + 1];
+            System.arraycopy(result, 0, bigger, 1, result.length);
+            bigger[0] = 0x01;
+            return bigger;
+        }
+        return result;
+    }
+
+    // no assumptions for zeros, parameter and result may have arbitrary amount of leading zeros
+    /*@ private static helper model \bigint simpleSum(int[] m) {
+      @     return (\sum int i; 0 <= i && i < m.length; toUnsigned(m[i]) * twopower(m.length-i-1));
+      @ }
+      @*/
+
+    // partial sum of the array, starting from startIndex (inclusive)
+    /*@ private model_behavior
+      @ accessible m[startIndex .. (m.length-1)];
+      @ private static helper model \bigint partialSum(int[] m, int startIndex) {
+      @     return (\sum int i;
+      @                  startIndex <= i && i < m.length;
+      @                  toUnsigned(m[i]) * twopower(m.length-i-1));
+      @ }
+      @*/
+
+    /**
+     * Subtracts the contents of the second int arrays (little) from the
+     * first (big).  The first int array (big) must represent a larger number
+     * than the second.  This method allocates the space necessary to hold the
+     * answer.
+     */
+    /*@ private normal_behavior
+      @ requires calcMagSum(big) > calcMagSum(little);
+      @ requires (big.length > 0 ==> big[0] != 0) && (little.length > 0 ==> little[0] != 0);
+      @ ensures simpleSum(\result) == simpleSum(big) - simpleSum(little);   // may have leading zeros
+      @ assignable \nothing;
+      @*/
+    private static /*@ helper @*/ int[] subtract(int[] big, int[] little) {
+        int bigIndex = big.length;
+        int result[] = new int[bigIndex];
+        int littleIndex = little.length;
+        long difference = 0;
+
+        // Subtract common parts of both numbers
+        /*@ loop_invariant 0 <= littleIndex && littleIndex <= little.length
+          @             && 0 <= bigIndex && bigIndex <= big.length
+          @             && big.length - bigIndex == little.length - littleIndex
+          @             && partialSum(result, bigIndex)
+          @                + (difference>>32)*twopower(big.length-bigIndex) // borrow from next digit
+          @               == partialSum(big, bigIndex)
+          @                - partialSum(little, littleIndex);
+          @ assignable result[(result.length-little.length)..(result.length-1)];
+          @ decreases littleIndex;
+          @*/
+        while (littleIndex > 0) {
+            difference = (big[--bigIndex] & LONG_MASK) -
+                         (little[--littleIndex] & LONG_MASK) +
+                         (difference >> 32);
+            result[bigIndex] = (int)difference;
+        }
+
+        // Subtract remainder of longer number while borrow propagates
+        boolean borrow = (difference >> 32 != 0);
+        /*@ loop_invariant 0 <= bigIndex && bigIndex <= big.length
+          @                && partialSum(result, bigIndex)
+          @                 == partialSum(big, bigIndex) - partialSum(little, 0)
+          @                    + (borrow ? twopower(big.length-bigIndex) : (\bigint)0);
+          @ assignable result[*];
+          @ decreases bigIndex;
+          @*/
+        while (bigIndex > 0 && borrow)
+            borrow = ((result[--bigIndex] = big[bigIndex] - 1) == -1);
+            /* --bigIndex;
+             * result[bigIndex] = big[bigIndex] - 1;
+             * borrow = (big[bigIndex] == 0);
+             */
+
+        // Copy remainder of longer number
+        /*@ loop_invariant bigIndex >= 0
+          @             && partialSum(result, bigIndex) == partialSum(big, bigIndex)
+          @                                              - partialSum(little, 0);
+          @ assignable result[*];
+          @ decreases bigIndex;
+          @*/
+        while (bigIndex > 0)
+            result[--bigIndex] = big[bigIndex];
+
+        return result;
+    }
+
+    /**
+     * Throws an {@code ArithmeticException} if the {@code BigInteger} would be
+     * out of