hermetic
发表于 2025-3-27 00:38:32
Perluette : A compilers producing system using abstract data types,compilers producing system Perluette. This system is based upon a formal semantics of programming languages. Programming languages are considered to be algebraic data types. Then it becomes possible to specify and prove their implementations as representations of an algebraic data type into another
流利圆滑
发表于 2025-3-27 02:18:13
http://reply.papertrans.cn/48/4721/472056/472056_32.png
PARA
发表于 2025-3-27 05:47:24
Another characterization of weakest preconditions,e input-output behaviour of programs. These relations include an explicit representation of non-terminating computations. Based on the relational model we introduce a weakest precondition total correctness predicate transformer. We then show how to build up this predicate transformer starting from o
Immunotherapy
发表于 2025-3-27 10:09:42
http://reply.papertrans.cn/48/4721/472056/472056_34.png
Phagocytes
发表于 2025-3-27 16:35:30
Optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-lissor. We adopt a simplified model of a multiprocessor, consisting of several identical processors, all sharing access to a common memory. Synchronization must be done explicitly, using two special operations that take a period of time comparable to the cost of data operations. Our treatment differs
FANG
发表于 2025-3-27 18:50:12
http://reply.papertrans.cn/48/4721/472056/472056_36.png
Intact
发表于 2025-3-28 01:23:32
Proving the correctness of implementations of shared data abstractions,nsion of Hoare‘s method developed for proving the correctness of an implementation of abstract data types specified in a sequential programming environment. An example is given to illustrate the proposed proof method.
夹死提手势
发表于 2025-3-28 02:51:16
http://reply.papertrans.cn/48/4721/472056/472056_38.png
PUT
发表于 2025-3-28 07:51:49
Tuning algebraic specifications by type merging,ave the disadvantage of being too much decomposed and hence not directly suited for finding efficient implementations. The paper presents a formal method for overcoming this drawback by combining suitable hierarchical types while simultaneously specifying new (combined) operations.
值得赞赏
发表于 2025-3-28 11:43:32
An enlarged definition and complete axiomatization of observational congruence of finite processes,gruence ; a finite set of equational axioms is given for the congruence, which we prove to be a complete proof system by argumenting over canonical forms of programs. In a second time, our language is enriched by adding it the necessary operators for expressing the parallel composition of processes