close
1.

図書

図書
Peter Müller
出版情報: Berlin : Springer, c2002  xiv, 292 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2262
所蔵情報: loading…
目次情報: 続きを見る
Introduction / 1:
Motivation / 1.1:
Specification and Verification Technique / 1.2:
The Problem / 1.3:
Modular Correctness / 1.3.1:
The Frame Problem / 1.3.2:
Modular Verification of Type Invariants / 1.3.3:
The Extended State Problem / 1.3.4:
Alias Control / 1.3.5:
Modularity Aspects of Programs, Specifications, and Proofs / 1.4:
Modularity of Programs / 1.4.1:
Modularity of Universal Specifications / 1.4.2:
Modularity of Interface Specifications / 1.4.3:
Modularity of Correctness Proofs / 1.4.4:
Approach, Outline, and Contributions / 1.5:
Approach / 1.5.1:
Outline / 1.5.2:
Contributions / 1.5.3:
Related Work / 1.6:
Specification Techniques / 1.6.1:
Verification and Analysis Techniques / 1.6.2:
Mojave and the Universe Type System / 2:
Mojave: The Language / 2.1:
The Language Core / 2.1.1:
Modularity / 2.1.2:
Universes: A Type System for Flexible Alias Control / 2.2:
The Ownership Model / 2.2.1:
The Universe Programming Model / 2.2.2:
Programming with Universes / 2.2.3:
Examples / 2.2.4:
Formalization of the Universe Type System / 2.2.5:
Discussion / 2.2.6:
The Semantics of Mojave / 2.3:
Programming Logic / 3.1:
Formal Data and State Model / 3.1.1:
Axiomatic Semantics / 3.1.2:
Language Properties / 3.1.3:
Type Safety / 3.2.1:
Liveness Properties / 3.2.2:
Properties of Readonly Methods / 3.2.3:
Correctness / 3.3:
Correctness of Closed Programs / 3.3.1:
Correctness of Open Programs: Modular Correctness / 3.3.2:
Modular Soundness / 3.3.3:
Composition of Modular Correct Open Programs / 3.3.4:
Modular Specification and Verification of Functional Behavior / 3.4:
Foundations of Interface Specifications / 4.1:
Specification of Functional Behavior / 4.2:
Abstract Fields / 4.2.1:
Pre-post-specifications / 4.2.2:
Verification of Functional Behavior / 4.3:
Verification of Method Bodies / 4.3.1:
Proofs for Virtual Methods / 4.3.2:
Example / 4.3.3:
Modular Specification and Verification of Frame Properties / 4.4:
Meaning of Modifies-Clauses / 5.1:
Explicit Dependencies / 5.1.2:
Modularity Rules / 5.1.3:
Formalization of Explicit Dependencies / 5.2:
Declaration of Dependencies / 5.2.1:
Axiomatization of the Depends-Relation / 5.2.2:
Consistency with Representation / 5.2.3:
Formalization of the Modularity Rules / 5.2.4:
Axiomatization of the Notdepends-Relation / 5.2.5:
Formalization of Modifies-Clauses / 5.2.6:
Verification of Frame Properties / 5.4:
Local Update Property / 5.4.1:
Accessibility Properties / 5.4.3:
Modularity Theorem for Frame Properties / 5.4.4:
Leino's and Nelson's Work on Dependencies / 5.4.5:
Other Work on the Frame Problem / 5.5.2:
Modular Specification and Verification of Type Invariants / 6:
Motivation and Approach / 6.1:
Invariant Semantics for Nonmodular Programs / 6.1.1:
Problems for Modular Verification of Invariants / 6.1.2:
Specification of Type Invariants / 6.1.3:
Declaration of Type Invariants / 6.2.1:
Formal Meaning of Invariants / 6.2.2:
Verification of Type Invariants / 6.3:
Verification Methodology / 6.3.1:
Module Invariants / 6.3.2:
History Constraints / 6.4.2:
Conclusion / 6.5:
Summary and Contributions / 7.1:
The Lopex Project / 7.2:
Tool Support / 7.3:
Directions for Future Work / 7.4:
Formal Background and Notations / A:
Formal Background / A.1:
Notations / A.2:
Predefined Type Declarations / B:
Doubly Linked List / C:
Property Editor / C.2:
Auxiliary Lemmas, Proofs, and Models / D:
Auxiliary Lemmas and Proofs from Chapter 3 / D.1:
Auxiliary Lemmas and Proofs from Chapter 5 / D.2:
Auxiliary Lemmas and Proofs from Chapter 6 / D.3:
A Model for the Axiomatization of the Depends-Relation / D.4:
Bibliography
List of Figures
Index
Introduction / 1:
Motivation / 1.1:
Specification and Verification Technique / 1.2:
2.

電子ブック

EB
Peter Müller, Takeo Kanade
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2010
所蔵情報: loading…
目次情報: 続きを見る
Fine-Grain Concurrency / Tony Hoare
Compensable Transactions
SCOOP-A Contract-Based Concurrent Object-Oriented Programming Model / Benjamin Morandi ; Sebastian S. Bauer ; Bertrand Meyer
Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs / K. Rustan M. Leino ; Peter Müller
Fixpoints and Search in PVS / Natarajan Shankar
Multi Core Design for Chip Level Multiprocessing / Tryggve Fossum
Author Index
Fine-Grain Concurrency / Tony Hoare
Compensable Transactions
SCOOP-A Contract-Based Concurrent Object-Oriented Programming Model / Benjamin Morandi ; Sebastian S. Bauer ; Bertrand Meyer
3.

電子ブック

EB
Peter Müller
出版情報: Cambridge University Press Online Books , Leiden : Cambridge University Press, 2006
所蔵情報: loading…
目次情報: 続きを見る
Introduction / 1:
Equilibrium thermodynamics of sea water / 2:
Balance equations / 3:
Molecular flux laws / 4:
The gravitational potential / 5:
The basic equations / 6:
Dynamical impact of the equation state / 7:
Free wave solution on a sphere / 8:
Asymptotic expansions / 9:
Reynolds decomposition / 10:
Boussinesq approximation / 11:
Large scale motions / 12:
Primitive equations / 13:
Representations of vertical structure / 14:
Ekman layers / 15:
Planetary geostrophic flows / 16:
Tidal equations / 17:
Medium scale motions / 18:
Quasi-geostrophic flows / 19:
Motions on the f-plane / 20:
Small scale motions / 21:
Sound waves / 22:
Equilibrium thermodynamics / A:
Vector and tensor analysis / B:
Orthogonal curvilinear coordinate systems / C:
Kinematics of fluid motions / D:
Kinematics of waves / E:
Conventional and notation / F:
References
Index
Introduction / 1:
Equilibrium thermodynamics of sea water / 2:
Balance equations / 3:
4.

電子ブック

EB
Peter Müller
出版情報: SpringerLink Books Mathematics And Statistics Without Lecture Notes 2015 , Springer International Publishing, 2015
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼