pith. sign in

arxiv: 1907.03723 · v2 · pith:QEXADEFSnew · submitted 2019-07-08 · 💻 cs.SE

APML: An Architecture Proof Modeling Language

Diego Marmsoler , Genc Blakqori This is my paper

Pith reviewed 2026-05-25 00:57 UTC · model grok-4.3

classification 💻 cs.SE
keywords architecture proof modelingcompositional verificationmessage sequence chartsarchitecture contractsproof sketchingsoftware architecturetheorem proving
0
0 comments X

The pith

APML lets architects sketch proofs about how components compose using message sequence chart notations that are sound and complete for contract verification and map to full theorem-prover scripts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents APML as a language that lets architects draw proof sketches for component compositions at the architecture level instead of working directly in a full interactive theorem prover. The sketches use notations similar to message sequence charts, and the authors prove the language is sound and complete for checking architecture contracts. An algorithm is given that converts any valid APML sketch into a corresponding detailed proof script. The work includes an Eclipse-based implementation, a running example, and evaluation on a larger case study that also surfaces some limits.

Core claim

APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. The language is sound and complete for the verification of architecture contracts, and there is an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover.

What carries the argument

The APML language itself, defined with message-sequence-chart-like diagram notation, together with its soundness and completeness theorems for architecture contracts and the algorithm that translates sketches into interactive theorem-prover scripts.

If this is right

  • Component verification by model checking can be paired with composition verification by architect-drawn sketches.
  • Architects without theorem-prover training can still produce checkable proofs of how components fit together.
  • Proof sketches at the architecture level can be expanded automatically into full verifiable scripts.
  • The approach can be used inside standard modeling tools such as the Eclipse-based implementation described.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same sketch-and-map pattern might apply to other compositional reasoning tasks outside software architecture.
  • Limitations noted in the case study point to possible extensions that increase the range of interactions the diagrams can capture.
  • Tighter coupling between the sketch language and single-component model checkers could reduce manual translation steps.

Load-bearing premise

Notations similar to message sequence charts can express all essential structures of component composition proofs without omitting information required for a complete theorem-prover verification.

What would settle it

An architecture contract that has a valid composition proof yet admits no APML diagram whose mapping produces a correct theorem-prover script, or an APML diagram that maps to an invalid script.

Figures

Figures reproduced from arXiv: 1907.03723 by Diego Marmsoler, Genc Blakqori.

Figure 1
Figure 1. Figure 1: A typical Isabelle locale. Specifications in Isabelle are grouped into so￾called theories, which may import other theories. To modularize results, Isabelle supports the de￾velopment of abstract specifications by means of locales [3] [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A typical Isabelle/Isar proof. In Isabelle, proofs can be ex￾pressed in a natural way using Isabelle’s structured proof lan￾guage Isar [43]. A typical Isar proof is depicted in fig. 2: It con￾sists of a sequence of proof steps, which are discharged by some proof methods. For example, Is￾abelle’s classical reasoner blast can perform long chains of reasoning steps to prove formulas. Or the simplifier simp ca… view at source ↗
Figure 3
Figure 3. Figure 3: Architecture for a reliable adder. The behavior of each component is specified in terms of contracts (as introduced by definition 6) by the sequence diagrams depicted in fig. 4: Figure 4a depicts contract dispatch for the dispatcher component. It requires a dispatcher to forward incoming messages received at ports i1 and i2, on its output ports o1 − o4, within one time unit. The contracts for the two adder… view at source ↗
Figure 4
Figure 4. Figure 4: Contracts for components of reliable adder. [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Contract for reliable adder. Note that our running example is deliberately oversimplified, since its main purpose is to demon￾strate our concepts and ideas rather than evaluat￾ing the approach in a real world scenario. For details about how the approach works on a real example, we refer to the description of the case study in section 7. 4 Modeling Architecture Proofs An architecture contract can be verifie… view at source ↗
Figure 6
Figure 6. Figure 6: Architecture proof by means of Message Sequence Chart. [PITH_FULL_IMAGE:figures/full_fig_p010_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: depicts the specification of our running example in FACTUM Studio: First, the architecture is specified graphically in terms of interfaces (represented as gray rectangles) and connections between their input (empty circles) and output (filled circles) ports. Then, contracts can be added for each component using a textual notation [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: APML proof in FACTUM Studio [PITH_FULL_IMAGE:figures/full_fig_p013_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Automatic Train Control System 7 Case Study: Trainguard MT Control System We evaluated our approach by applying it for the verification of a railway-control system. To investigate whether the approach can indeed be used to apply interactive theorem proving by users not trained in using this technology, verification was performed by a subject with no prior experience with formal methods in general and speci… view at source ↗
Figure 10
Figure 10. Figure 10: Number of proof steps for each property [PITH_FULL_IMAGE:figures/full_fig_p014_10.png] view at source ↗
read the original abstract

To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while this does not seem to be the case in general the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces APML, a modeling language using notations similar to Message Sequence Charts for sketching proofs about component composition at the architecture level. It describes the language syntax and semantics, claims to establish soundness and completeness with respect to architecture contract verification, provides an algorithm mapping APML proofs to corresponding Isabelle proofs, presents an Eclipse/EMF implementation, and evaluates via a running example plus a larger case study.

Significance. If the mapping algorithm is semantics-preserving, APML would usefully bridge architecture-level reasoning with interactive theorem proving, allowing non-ITP experts to produce verifiable sketches. The explicit algorithm, implementation, and case-study evaluation are concrete strengths that could support adoption in compositional verification workflows.

major comments (2)
  1. [Mapping algorithm and soundness/completeness sections] The central soundness and completeness claims for APML rest on the mapping algorithm to Isabelle (described after the language definition). No machine-checked metatheorem or detailed inductive argument is supplied showing that every valid APML diagram produces a valid Isabelle proof (and conversely), leaving open the possibility that implicit well-formedness conditions or unstated side conditions on diagrams are required.
  2. [Language definition and case study] The weakest assumption—that MSC-style diagrams are expressive enough to capture all necessary proof obligations for component contracts without loss of detail—is invoked in the language description and mapping but is not subjected to a concrete counter-example search or completeness argument against a representative set of Isabelle contract proofs.
minor comments (2)
  1. Notation for diagram elements (e.g., message labels, contract assertions) should be defined in a single table or figure caption for quick reference.
  2. [Case study] The case-study limitations paragraph would benefit from explicit enumeration of which contract patterns could not be expressed in APML.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive review and for highlighting both the potential strengths and the areas requiring clarification in our manuscript on APML. We address each major comment below, indicating where revisions will be made to strengthen the presentation of the soundness and completeness arguments.

read point-by-point responses

  1. Referee: [Mapping algorithm and soundness/completeness sections] The central soundness and completeness claims for APML rest on the mapping algorithm to Isabelle (described after the language definition). No machine-checked metatheorem or detailed inductive argument is supplied showing that every valid APML diagram produces a valid Isabelle proof (and conversely), leaving open the possibility that implicit well-formedness conditions or unstated side conditions on diagrams are required.

    Authors: The manuscript presents the mapping algorithm as the core mechanism establishing the correspondence between APML diagrams and Isabelle proofs, with soundness and completeness argued via the semantics-preserving construction of the algorithm. We agree that a more explicit inductive argument, including discussion of well-formedness conditions on diagrams, would make the metatheory more rigorous and address potential implicit assumptions. In the revised version we will add a dedicated subsection providing a detailed (though not machine-checked) sketch of the inductive argument for both directions of the correspondence. revision: yes

  2. Referee: [Language definition and case study] The weakest assumption—that MSC-style diagrams are expressive enough to capture all necessary proof obligations for component contracts without loss of detail—is invoked in the language description and mapping but is not subjected to a concrete counter-example search or completeness argument against a representative set of Isabelle contract proofs.

    Authors: The running example and larger case study provide concrete demonstrations that APML can capture the necessary proof obligations in the chosen domain without apparent loss of detail. We acknowledge, however, that these do not constitute a systematic counter-example search or a formal completeness argument relative to an arbitrary set of Isabelle proofs. In revision we will expand the language definition and evaluation sections to include an explicit discussion of this assumption, any identified limitations on expressiveness, and a brief analysis of how the case study relates to broader completeness considerations. revision: yes

Circularity Check

0 steps flagged

No circularity: APML soundness/completeness and mapping are definitional results shown within the paper

full rationale

The paper defines a new language APML, states that it shows soundness and completeness for architecture contracts, and provides a mapping algorithm to Isabelle proofs. These are presented as direct results of the language definition and associated metatheory rather than any reduction to fitted parameters, self-referential citations, or renamed inputs. No load-bearing step equates a claimed prediction or theorem to its own construction by definition. The case study and implementation are separate from the core claims.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on the semantic definition of APML, the soundness/completeness theorems, and the correctness of the mapping algorithm to Isabelle. No free parameters are mentioned. Axioms include standard mathematical properties of the underlying logic and domain assumptions about what constitutes an architecture contract.

axioms (2)
  • standard math Standard properties of the underlying logic used in Isabelle (e.g., higher-order logic semantics)
    Invoked when claiming the mapping produces valid Isabelle proofs.
  • domain assumption Architecture contracts can be adequately represented using notations similar to Message Sequence Charts
    This is the core modeling choice that enables the language design.

pith-pipeline@v0.9.0 · 5735 in / 1405 out tokens · 18545 ms · 2026-05-25T00:57:33.949582+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    Mathemati- cal structures in computer science 14(03), 329–366 (2004)

    Arbab, F.: Reo: a channel-based coordination model for component composition. Mathemati- cal structures in computer science 14(03), 329–366 (2004)

    work page 2004

  2. [2]

    Mit Press, MIT Press (2008), https://books.google.de/books?id=nDQiAQAAIAAJ

    Baier, C., Katoen, J., Larsen, K.: Principles of Model Checking. Mit Press, MIT Press (2008), https://books.google.de/books?id=nDQiAQAAIAAJ

    work page 2008

  3. [3]

    Lecture notes in computer science 3085, 34–50 (2004)

    Ballarin, C.: Locales and locale expressions in Isabelle/Isar. Lecture notes in computer science 3085, 34–50 (2004)

    work page 2004

  4. [4]

    Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al.: The Coq proof assistant reference manual: Version 6.1. Ph.D. thesis, Inria (1997)

    work page 1997

  5. [5]

    Packt Publishing Ltd (2016)

    Bettini, L.: Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd (2016)

    work page 2016

  6. [6]

    In: International conference on tools and algorithms for the construction and analysis of systems

    Biere, A., Cimatti, A., Clarke, E., Zhu, Y .: Symbolic model checking without BDDs. In: International conference on tools and algorithms for the construction and analysis of systems. pp. 193–207. Springer (1999)

    work page 1999

  7. [7]

    In: International Conference on Computer Aided Verification

    Bobaru, M.G., P˘as˘areanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: International Conference on Computer Aided Verification. pp. 135–148. Springer (2008)

    work page 2008

  8. [8]

    Formal Methods in System Design 52(1), 33–87 (2018), https://doi.org/10.1007/s10703-017-0304-9

    Broy, M.: Theory and methodology of assumption/commitment based system interface speci- fication and architectural contracts. Formal Methods in System Design 52(1), 33–87 (2018), https://doi.org/10.1007/s10703-017-0304-9

    work page doi:10.1007/s10703-017-0304-9 2018

  9. [9]

    Springer Science & Business Media (2012)

    Broy, M., Stølen, K.: Specification and development of interactive systems:FOCUS on streams, interfaces, and refinement. Springer Science & Business Media (2012)

    work page 2012

  10. [10]

    In: Carreño, V .A., Muñoz, C.A., Tahar, S

    Brucker, A.D., Wolff, B.: A proposal for a formal OCL semantics in Isabelle/HOL. In: Carreño, V .A., Muñoz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Order Logics. pp. 99–114. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)

    work page 2002

  11. [11]

    In: International Workshop on Formal Aspects of Component Software

    Chilton, C., Jonsson, B., Kwiatkowska, M.: Assume-guarantee reasoning for safe component behaviours. In: International Workshop on Formal Aspects of Component Software. pp. 92–109. Springer (2012)

    work page 2012

  12. [12]

    In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE)

    Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: A tool for checking the refinement of tempo- ral contracts. In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 702–705 (Nov 2013)

    work page 2013

  13. [13]

    Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97(P3), 333–348 (Jan 2015), http://dx.doi.org/10. 1016/j.scico.2014.06.011

    work page 2015

  14. [14]

    In: [1989] Pro- ceedings

    Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: [1989] Pro- ceedings. Fourth Annual Symposium on Logic in Computer Science. pp. 353–362. IEEE (1989)

    work page 1989

  15. [15]

    Formal methods in system design 19(1), 45–80 (2001)

    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal methods in system design 19(1), 45–80 (2001)

    work page 2001

  16. [16]

    In: 2011 Design, Automation & Test in Europe

    Damm, W., Hungar, H., Josko, B., Peikenkamp, T., Stierand, I.: Using contract-based com- ponent specifications for virtual integration testing and architecture design. In: 2011 Design, Automation & Test in Europe. pp. 1–6. IEEE (2011)

    work page 2011

  17. [17]

    Com- mun

    De Moura, L., Bjørner, N.: Satisfiability modulo theories: Introduction and applications. Com- mun. ACM 54(9), 69–77 (Sep 2011), http://doi.acm.org/10.1145/1995376. 1995394

    work page doi:10.1145/1995376 2011

  18. [18]

    In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat

    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No. 99CB37002). pp. 411–420. IEEE (1999) 16

    work page 1999

  19. [19]

    In: Bjørner, N., de Boer, F.S

    Elkader, K.A., Grumberg, O., Pasareanu, C.S., Shoham, S.: Automated circular assume- guarantee reasoning. In: Bjørner, N., de Boer, F.S. (eds.) FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9109, pp. 23–39. Springer (2015), https://doi.org/10. 1007/978-3-319-19249-9_3

    work page 2015

  20. [20]

    In: Cuéllar, J., Maibaum, T.S.E., Sere, K

    Emmi, M., Giannakopoulou, D., Pasareanu, C.S.: Assume-guarantee verification for interface automata. In: Cuéllar, J., Maibaum, T.S.E., Sere, K. (eds.) FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5014, pp. 116–131. Springer (2008), https: //doi...

    work page doi:10.1007/978-3-540-68237-0_10 2008

  21. [21]

    In: Automated Software Engineering

    Fensel, D., Schnogge, A.: Using KIV to specify and verify architectures of knowledge-based systems. In: Automated Software Engineering. pp. 71–80 (Nov 1997)

    work page 1997

  22. [22]

    In: Naumann, D

    Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: A mechanised theory engineering frame- work. In: Naumann, D. (ed.) Unifying Theories of Programming. pp. 21–41. Springer Interna- tional Publishing, Cham (2015)

    work page 2015

  23. [23]

    Hoare, C.A.R., Jifeng, H.: Unifying theories of programming, vol. 14. Prentice Hall Engle- wood Cliffs (1998)

    work page 1998

  24. [24]

    In: International Symposium on Formal Techniques in Real-Time and Fault- Tolerant Systems

    Huber, F., Schätz, B., Schmidt, A., Spies, K.: Autofocus—a tool for distributed systems specification. In: International Symposium on Formal Techniques in Real-Time and Fault- Tolerant Systems. pp. 467–470. Springer (1996)

    work page 1996

  25. [25]

    In: 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016, Kanpur, India, November 18-20, 2016

    Kugele, S., Marmsoler, D., Mata, N., Werther, K.: Verification of component architectures us- ing mode-based contracts. In: 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016, Kanpur, India, November 18-20, 2016. pp. 133–142. IEEE (2016), https://doi.org/10.1109/MEMCOD.2016.7797758

    work page doi:10.1109/memcod.2016.7797758 2016

  26. [26]

    In: Fiadeiro, J.L., Liu, Z., Xue, J

    Li, Y ., Sun, M.: Modeling and analysis of component connectors in Coq. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) Formal Aspects of Component Software - 10th International Symposium, FACS 2013, Nanchang, China, October 27-29, 2013, Revised Selected Papers. Lecture Notes in Computer Science, vol. 8348, pp. 273–290. Springer (2013), https://doi.org/10. 10...

    work page 2013

  27. [27]

    Scientific Annals of Computer Science 26(2), 187–248 (2016)

    Marmsoler, D., Gleirscher, M.: On activation, connection, and behavior in dynamic architec- tures. Scientific Annals of Computer Science 26(2), 187–248 (2016)

    work page 2016

  28. [28]

    In: The 20th International Conference on Formal Engineering Methods, ICFEM 2018, Proceedings (2018)

    Marmsoler, D.: A framework for interactive verification of architectural design patterns in Isabelle/HOL. In: The 20th International Conference on Formal Engineering Methods, ICFEM 2018, Proceedings (2018)

    work page 2018

  29. [29]

    Marmsoler, D.: Hierarchical specication and verication of architecture design patterns. In: Fundamental Approaches to Software Engineering - 21th International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (2018)

    work page 2018

  30. [30]

    Software Engineering und Software Management 2019 (2019)

    Marmsoler, D.: Verifying dynamic architectures using model checking and interactive theorem proving. Software Engineering und Software Management 2019 (2019)

    work page 2019

  31. [31]

    In: International Conference on Formal Aspects of Component Software

    Marmsoler, D., Gidey, H.K.: FACTUM Studio: A tool for the axiomatic specification and verification of architectural design patterns. In: International Conference on Formal Aspects of Component Software. pp. 279–287. Springer (2018)

    work page 2018

  32. [32]

    In: International Colloquium on Theoretical Aspects of Computing, pp

    Marmsoler, D., Gleirscher, M.: Specifying properties of dynamic architectures using configu- ration traces. In: International Colloquium on Theoretical Aspects of Computing, pp. 235–254. Springer (2016)

    work page 2016

  33. [33]

    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science & Business Media (2002)

    work page 2002

  34. [34]

    https://www.eclipse.org/sirius/ 17

    Obeo: Sirius. https://www.eclipse.org/sirius/ 17

    work page

  35. [35]

    In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking

    Pasareanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of soft- ware: A comparative case study. In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking. pp. 168–183. Springer-Verlag, Berlin, Heidelberg (1999), http://dl.acm.org/citation.cfm? id=645879.672067

    work page arXiv 1999

  36. [36]

    In: Logics and models of concurrent systems, pp

    Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems, pp. 123–144. Springer (1985)

    work page 1985

  37. [37]

    KORSO: Methods, Languages, and Tools for the Construction of Correct Software pp

    Reif, W.: The KIV-approach to software verification. KORSO: Methods, Languages, and Tools for the Construction of Correct Software pp. 339–368 (1995)

    work page 1995

  38. [38]

    Tagungsband der Net

    Reussner, R.H., Becker, S., Firus, V .: Component composition with parametric contracts. Tagungsband der Net. ObjectDays 2004, 155–169 (2004)

    work page 2004

  39. [39]

    In: 21 st International Conference on Theorem Proving in Higher Order Logics

    Spichkova, M.: FOCUS on Isabelle: From specification to verification. In: 21 st International Conference on Theorem Proving in Higher Order Logics. p. 104. Citeseer (2008)

    work page 2008

  40. [40]

    Pearson Education (2008)

    Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education (2008)

    work page 2008

  41. [41]

    Addison-Wesley object technology series (1998)

    Warmer, J.B., Kleppe, A.G.: The Object Constraint Language: Precise modeling with UML. Addison-Wesley object technology series (1998)

    work page 1998

  42. [42]

    Wenzel, M.: The Isabelle/Isar reference manual (2004)

    work page 2004

  43. [43]

    From Insight to Proof – Festschrift in Honour of Andrzej Trybulec 10(23), 277–298 (2007) 18 A Proof for Thm

    Wenzel, M.: Isabelle/Isar – a generic framework for human-readable proof documents. From Insight to Proof – Festschrift in Honour of Andrzej Trybulec 10(23), 277–298 (2007) 18 A Proof for Thm. 1 The following diagram depicts an overview of the main concepts and its relationships and marks the proof obligation with a question mark: A Kf k Bf A⊗B |= |= ? ps...

    work page 2007