Content deleted Content added
→References: typo |
|||
Line 8:
An [[array data structure|array]] can be specified by the following equational [[axiom]]:<ref group=note>Here, ''select''(''a'',''i'') informally designates the value of the ''i''th element of ''a'', written e.g. in [[C (programming language)|C]] as <code lang="C">a[i]</code>, while ''store''(''a'',''i'',''v'') informally designates the array resulting from writing the value ''v'' to the ''i''th element of ''a'', written in C as <code lang="C">a[i]=v</code>.
The axiom then informally means that the value obtained by the statements <code lang="C">a[i]=v;return a[j];</code> equals <code lang="C">v</code> if <code lang="C">i</code>=<code lang="C">j</code>, and <code lang="C">a[j]</code>, else.</ref>
: ''select''(''store''(''a'',''i'',''v''),''j'') = (if ''i'' = ''j'' then ''v'' else ''select''(''a'',''j''))
| |||