This section gives a formal proof of a valid edge-oriented communication between cells with the stack system using push and pop operations for the Sierpiński SFC. Using push operations on edges of type new and pop operations on edges of type old, the following theorem holds:
Theorem 4.7.1 (Valid stack-based communication) Using the communication schemes with the pop and push operations on the communication stack yields correct data transfer to each cell adjacent to the corresponding edge.
The proof of the theorem is supported by axiomatic rules closely related to those of the Hoare calculus [Hoa69]. We define inference rules given in the form with A stating the condition which has to hold true and B the condition to replace A. The conditions are given by a tuple of tuples {{P}S{Q}}^{n} with the precondition P, the code-statement S and the postcondition Q.
We further assume push and pop operations specified via push(S,a), pushing the element a to stack S, and pop(S,a) fetching element a from the stack.
The push and pop operations are extended with the pre- and postconditions
Correct communication: The success of a correct pop operation by applying the grammar and inheritance of types lead to pop operations pop(S,α), testing for correct fetching of element α from the top of the stack. This leads to the rule
| (4.15) |
This converts the pop operation into the pop operation introduced in Section 4.2, which allows
reduction:
Reduction: Correct communication via push/pop to/from stack S^{k} is recognized and reduced via
| (4.16) |
This assures correct communication information received by the communication partner by pushing the same data α to the stack and fetching the same data α from the same stack. A reduction statement tests for such a correct communication and removes the statements, resulting in ϵ. We are allowed to do so, since the stack is kept in an unmodified state for all other edges accesses.
Commutativity: Commutative property for accessing different communication stacks
Joining consecutive communication data: In case of pushing or fetching edge data in the correct order with respect to the parent triangle allows to join data stored on the stack:
We apply the rules R1-R8 to show the valid stack access for edge-based communication. Considering only new and old communication types, the proof is given without loss of generality by boundary edges assumed to not modify any communication stacks. For even traversals, the access order for the root triangle only considering the edge access (see Section 4.3.2) is given by
We map each new and old communication type of edge data α to push(S^{k},α) and pop(S^{k},α) to/from stack S^{k}. To avoid verification for all push/pop combinations, we use a generalization of stack operations
For the parent element of type even, this leads to the push and pop operations
Our communication scheme with type inheritance
With our grids generated by the spacetree, we still have to prove the stack system for an entire grid. Without loss of generality, we only present this proof for diamond-shaped grid areas by applying coarsening rules, see Fig. 4.11.
We assemble two half-diamond operations (see Eqs. (4.20)) to operations of a full diamond and apply the coarsening operations. With operations on the right stack access represented by the symbol [X], this yields the following code
Theorem 4.7.2 (SFC stack communication order) We consider a traversal with stack-based communication and communicate the cell identifiers I_{i} via edges. Here, the identifiers I_{i} are increasing by traversing the cells following the SFC. Then it holds that at any time during the traversal all identifiers are ordered on the communication stack.
We just introduced a method for validating the correct communication via the left- and right stacks for two-dimensional triangular grids. Such a way of validation can play an important role on the search for valid stack-communication properties for other SFC-induced grids such as hexagons or higher-dimensional shapes.