Java Reference
In-Depth Information
Listing 3-37.
Verifying a postcondition as well as preconditions
class MergeArrays
{
public static void main(String[] args)
{
int[] x = { 1, 2, 3, 4, 5 };
int[] y = { 1, 2, 7, 9 };
int[] result = merge(x, y);
for (int i = 0; i < result.length; i++)
System.out.println(result[i]);
}
static int[] merge(int[] a, int[] b)
{
if (a == null)
throw new nullPointerException("a is null");
if (b == null)
throw new nullPointerException("b is null");
int[] result = new int[a.length+b.length];
// Precondition
assert result.length == a.length+b.length: "length
mismatch";
for (int i = 0; i < a.length; i++)
result[i] = a[i];
for (int i = 0; i < b.length; i++)
result[a.length+i-1] = b[i];
// Postcondition
assert containsAll(result, a, b): "value missing from
array";
return result;
}
static boolean containsAll(int[] result, int[] a, int[]
b)
{
for (int i = 0; i < a.length; i++)
if (!contains(result, a[i]))
return false;
