		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Double-array-write

Write a component to a Java double array.

Signature
(double-array-write array index component) → new-array
Arguments: array — Guard (double-arrayp array).; index — Guard (int-valuep index).; component — Guard (double-valuep component).
Returns: new-array — Type (double-arrayp new-array).

Definitions and Theorems

Function: double-array-write

(defun double-array-write (array index component)
  (declare (xargs :guard (and (double-arrayp array)
                              (int-valuep index)
                              (double-valuep component))))
  (declare
       (xargs :guard (double-array-index-in-range-p array index)))
  (let ((__function__ 'double-array-write))
    (declare (ignorable __function__))
    (if (mbt (double-array-index-in-range-p array index))
        (double-array (update-nth (int-value->int index)
                                  component
                                  (double-array->components array)))
      (double-array-fix array))))

Theorem: double-arrayp-of-double-array-write

(defthm double-arrayp-of-double-array-write
  (b* ((new-array (double-array-write array index component)))
    (double-arrayp new-array))
  :rule-classes :rewrite)

Theorem: len-of-components-of-double-array-write

(defthm len-of-components-of-double-array-write
  (b* ((?new-array (double-array-write array index component)))
    (equal (len (double-array->components new-array))
           (len (double-array->components array)))))

Theorem: double-array-index-in-range-p-of-double-array-write

(defthm double-array-index-in-range-p-of-double-array-write
  (b* ((?new-array (double-array-write array index component)))
    (equal (double-array-index-in-range-p new-array index1)
           (double-array-index-in-range-p array index1))))