[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem ArrayMax-class
package
swt
;
public
class
ArrayMax
extends
java.lang
.
Object
{ swt.ArrayMax() { super(); }
public
static
int
max
(
int[]
a
) { int i = 0; int i0 = a.length - 1; while (i != i0) { if (a[i] <= a[i0]) i++; else i0--; }return i; } }
Validity: The proof is valid.
Features:
Comment: java type declarations
Used by:
Used by units in proved state:
Proof exists?: No