Overthrow
发表于 2025-3-25 07:19:47
Programs, Proofs and Parametrized Specifications,d Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces . programs that meet their Specifications.
伸展
发表于 2025-3-25 08:00:43
Towards Trustworthy Specification I: Consistency Checks,y proofs along the given specification structure, so that only in rather few remaining focus points, actual theorem proving is required. The practical usability of the resulting calculus is demonstrated by extensive examples taken from the C. library of basic data types.
Anticonvulsants
发表于 2025-3-25 14:37:23
The Common Framework Initiative for Algebraic Specification and Development of Software: Recent Prouirements and modular software design which subsumes many previous algebraic Specification languages. This paper is a brief summary of progress on CoFI during the period 1998-2001, when CoFI received funding from the European Commission as a Working Group under the Esprit programme.
松鸡
发表于 2025-3-25 18:58:45
,The Lübeck Transformation System: A Transformation System for Equational Higher Order Algebraic Speement modes covering the different transformation rules for entire specifications and single axioms. Finally we describe the architecture and the implementation of the system. Throughout the paper, we accompany the presentation with a running example.
DIKE
发表于 2025-3-25 22:18:58
http://reply.papertrans.cn/83/8234/823385/823385_25.png
Pericarditis
发表于 2025-3-26 02:24:02
http://reply.papertrans.cn/83/8234/823385/823385_26.png
insidious
发表于 2025-3-26 07:33:41
http://reply.papertrans.cn/83/8234/823385/823385_27.png
消音器
发表于 2025-3-26 09:15:25
http://reply.papertrans.cn/83/8234/823385/823385_28.png
头盔
发表于 2025-3-26 16:06:58
http://reply.papertrans.cn/83/8234/823385/823385_29.png
冒号
发表于 2025-3-26 17:24:50
Geometric Modelling with CASL,s been made easier by using different useful CASL features, like first-order logic, free types or structured specifications. Some assets of this specification are to be abstract, readable by researchers in geometric modelling and to simplify the programming process.