Nucleate
发表于 2025-3-25 06:55:46
Stepwise refinement and concurrency: A small exercise,A simple methodology for the design of concurrent programs is illustrated by a short example. This methodology formalizes the classical concept of “stepwise refinement”.
的是兄弟
发表于 2025-3-25 11:23:43
http://reply.papertrans.cn/63/6270/626968/626968_22.png
蛙鸣声
发表于 2025-3-25 12:02:29
The formal construction of a parallel triangular system solver,A parallel program for the solution of a triangular system of equations is formally derived. The program assumes the grid distribution of the .×. triangular matrix across .=.. processes. The complexity is ../.+. (.), both for a complete and for a square mesh communication network.
collagenase
发表于 2025-3-25 19:41:06
https://doi.org/10.1007/3-540-51305-1Computer; Hardware; Programmspezifikation und Transformation; Programmverifikation; Schrittweise Verfein
狗舍
发表于 2025-3-25 22:53:14
A formal approach to large SOFTWARE CONSTRUCTION,ich are quite different from those of the programming theory; in fact, we have not spoken of recursivity or algorithmics; on the other hand, we spoke of proofs..The design of a software system might be nothing else but the proof of its construction.
形状
发表于 2025-3-26 04:03:26
Specifications of concurrently accessed data,an be manipulated easily. This allowed us to derive several properties of the buffer (Appendix A) and construct a proof of buffer concatenation (Section 4). Also refinement of the specification with the eventual goal of implementation seems feasible with this scheme.
细颈瓶
发表于 2025-3-26 07:27:33
Stepwise refinement of action systems,rried out in the context of purely sequential programs. The resulting parallel algorithms can be efficiently executed on different architectures. The methodology is illustrated by showing the main derivation steps in a construction of a parallel algorithm for matrix multiplication.
图画文字
发表于 2025-3-26 08:54:07
A derivation of a systolic rank order filter with constant response time,rder filtering. The derivation proceeds in a calculational manner, originating from a formal specification and guided by performance considerations. The resulting solution is a linear systolic array of . cells, where . is the window size. It has constant response time and latency ..
墙壁
发表于 2025-3-26 14:00:39
http://reply.papertrans.cn/63/6270/626968/626968_29.png
反复拉紧
发表于 2025-3-26 17:46:52
Mathematics of Program Construction978-3-540-46191-3Series ISSN 0302-9743 Series E-ISSN 1611-3349