避开
发表于 2025-3-26 21:36:36
http://reply.papertrans.cn/63/6270/626956/626956_31.png
欺骗世家
发表于 2025-3-27 02:00:08
http://reply.papertrans.cn/63/6270/626956/626956_32.png
四海为家的人
发表于 2025-3-27 09:11:11
A compositional proof system for asynchronously communicating processes,formalism serves well as a basis for refinement and top-down development of distributed systems composed of asynchronously communicating processes. Moreover, we show that the first-order logic underlying the interface-specification language is decidable, which makes (semi-) automated verification more feasible.
条街道往前推
发表于 2025-3-27 11:51:19
http://reply.papertrans.cn/63/6270/626956/626956_34.png
Prosaic
发表于 2025-3-27 17:34:06
,Angelic termination in Dijkstra’s calculus,on proposal, the semantics are given by monotonic predicate transformers and monotonic operations on them. In this way the semantics of recursion is completely standard. The paper concludes with proof rules for recursive procedures and a small example of their applications.
STERN
发表于 2025-3-27 20:53:04
http://reply.papertrans.cn/63/6270/626956/626956_36.png
预感
发表于 2025-3-28 00:10:59
Conference proceedings 1995missions. The general theme is the use of crisp, clear mathematics in the discovery and design of algorithms and in the development of corresponding software and hardware; among the topics addressed are program transformation, program analysis, program verification, as well as convincing case studies.
Valves
发表于 2025-3-28 03:23:50
Towards automatic parallelization of logic programs,gram by generating the appropriate delay declarations, so that correctness is maintained and deadlock avoided. To this end we identify the crucial properties that the original Prolog program should satisfy and analyze which aspects of the parallelization process and of the correctness proof could be automated.
把手
发表于 2025-3-28 06:59:00
A simple, efficient, and flexible implementation of flexible arrays,without affecting time complexities. The standard flexible array operations take .(log . time, where . is the size of the flexible array. Additional operations, such as minimum and maximum take .(1) time.
注入
发表于 2025-3-28 12:56:26
An action system specification of the caltech asynchronous microprocessor,ecification. We propose a specification strategy that is based on the idea of . of the program variable space. Applying this strategy we give a completely formal derivation of a high level specification for the Caltech microprocessor. We also demonstrate the suitability of action systems and the stepwise refinement paradigm for ..