# How to define the dimension function for searching in a 3D-array?

Problem:

Propose a plan (pre- and post-condition, invariant, dimension function) for searching a value in a 3D-array.

Solution:

This is the first solution I've foreseen:

$[\text{Ctx}\ C: m\geqslant 0\wedge\ n\geqslant0\ \wedge\ p\geqslant0\ \wedge\ b[0..n-1,0..m-1,0..p-1]$

$\{\text{Pre}\ Q: T\}$

$\{\text{Inv}\ P: 0\leqslant i\leqslant n\ \wedge 0\leqslant j\leqslant n\ \wedge\ 0\leqslant k < p\ \wedge\$

$\}$

$\{\text{Dimension function}\ T: (m-1)*(n-1)-j\}$

$do\ ...\ od;$

$\{\text{Post}\ R: 0\leqslant i\leqslant n\ \wedge 0\leqslant j\leqslant n\ \wedge\ 0\leqslant k < p \wedge\ [(i=m\ \wedge\ x\in b)\ cor\ (i<m \wedge x=b[i,j,k]\ )]\}$

The matrix in this plan is part of the invariant: what it means is the actual searched area (green color).

Now, what I want to know is if the dimension function is sufficient to represent the remaining area to be searched in the $do$ loop.