遗产 发表于 2025-3-25 04:21:43
An object-based approach to the B formal method,ow how this is achieved. We prove formally that our design meets its informal specification with the help of B-Toolkit Release 3.3.1. We illustrate the approach by the B specification of A Computerized Visitor Information System (ACVIS). Using Object Modeling Technique diagrams allows us to make ACVIS more readable and open for changes.archetype 发表于 2025-3-25 10:16:18
http://reply.papertrans.cn/20/1930/192953/192953_22.pngavenge 发表于 2025-3-25 11:42:29
Durch Gleichungssysteme definierte Sprachenthe B method to support architectural abstractions, codifying the interactions of components. Finally, we present essential results of the case study and we show the significant impact of such a B formal development on the development process by giving some metrics.anus928 发表于 2025-3-25 17:17:06
https://doi.org/10.1007/978-3-319-44180-1 for getting confidence in these proofs and for administering the derivation steps. We have chosen the B-Method for this purpose. We propose how to extend the B-Method to make it more suitable for expressing the layers and assist in proving the corresponding superposition steps in a convenient way.defuse 发表于 2025-3-25 22:35:50
Introducing dynamic constraints in B, In a series of small appendices, we also give some theoretical foundations to our approach. In writing this paper, we have been heavily influenced by the pioneering works of Z. Manna and A. Pnueli , L. Lamport , R. Back and M. Butler .Grandstand 发表于 2025-3-26 02:16:16
http://reply.papertrans.cn/20/1930/192953/192953_26.pngARK 发表于 2025-3-26 05:58:38
http://reply.papertrans.cn/20/1930/192953/192953_27.pngHemodialysis 发表于 2025-3-26 11:17:51
Conference proceedings 1998nts 15 revised full papers selected from 29 submissions as well as four invited contributions. The B method is enjoying rapidly increasing popularity for the specification and design of software. The book covers all aspects of the B technology, including introductory and methodological issues, theor左右连贯 发表于 2025-3-26 16:09:23
The generalised substitution language extended to probabilistic programs,an be regarded as ‘the probability that . holds in the current state’. Then add explicit numbers and arithmetic operators, to give a richer language of arithmetic formulae into which predicates are embedded by 〈·〉..Abrial‘s generalised substitution language . can be applied to arithmetic rather thanhandle 发表于 2025-3-26 20:12:43
Well defined B,e ill-defined. Therefore the deduction system we use to discharge the proof obligations should be constructed from a three-valued logic. In this paper, we introduce a deduction system that allows to reason in a two-valued logic if new proof obligations called well-definedness lemmas are also proved.