| 摘要 |
This invention computes by constructing a lattice of states (figure 34). Every lattice of states (figure 6) corresponding to correct execution satisfies the temporal logic formula comprising a DANCE program (33). The invention integrates into a state-lattice (figure 34) computational model: a polymorphic strong type system; visibility-limiting domains; first-order assertions; and logic for providing a program correctness. This invention includes special hardware means (figure 24) for elimination of cache coherency among other things, necessary to construct state-lattices (figure 6) concurrently. The model of computation for the DANCE language consisting of four, interrelated, logical systems describing state-lattices (figure 6), types, domains (figure 42) and assertions. A fifth logical system (BPL) interrelates the other four systems allowing proofs of program correctness. The method of the present invention teaches programs as temporal formulas satisfied by lattices of states (figure 6) corresponding to correct execution. State-lattices (figure 6) that are short and bushy allow application of many processors simultaneously, thus reducing execution time.
|
