Defect Passivation towards Highly Efficient and Stable Metal Halide Perovskite Solar Cells

مرکز و کتابخانه مطالعات اسلامی به زبان های اروپایی

منو

" Defect Passivation towards Highly Efficient and Stable Metal Halide Perovskite Solar Cells "
Wang, Rui Yang, Yang

Document Type	:	BL
Record Number	:	727165
Doc. No	:	b546897
Main Entry	:	John V. Guttag; James J. Horning. With S.J. Garland ...
Title & Author	:	Larch Languages and Tools for Formal Specification\ John V. Guttag; James J. Horning. With S.J. Garland ...
Edition Statement	:	Softcover reprint of the hardcover 1st ed. 1993
Publication Statement	:	New York, NY [u.a.] Springer, [2012?]
Series Statement	:	Texts and Monographs in Computer Science
Page. NO	:	XIII, 250 S
ISBN	:	1461276365
	:	: 9781461276364
Contents	:	1 Specifications in Program Development.- 1.1 Programming with abstractions.- 1.2 Finding abstractions.- 1.3 The many roles of specification.- 1.4 Styles of specification.- 1.5 Formal specifications.- 2 A Little Bit of Logic.- 2.1 Basic logical concepts.- 2.2 Proof and consequences.- 3 An Introduction to Larch.- 3.1 Two-tiered specifications.- 3.2 LSL, the Larch Shared Language.- 3.3 Interface specifications.- 3.4 Relating implementations to specifications.- 3.5 LP, the Larch proof assistant.- 3.6 Lexical and typographic conventions.- 4 LSL: The Larch Shared Language.- 4.1 Equational specifications.- 4.2 Stronger theories.- 4.3 Combining traits.- 4.4 Renaming.- 4.5 Stating intended consequences.- 4.6 Recording assumptions.- 4.7 Built-in operators and overloading.- 4.8 Shorthands.- 4.9 Further examples.- 5 LCL: A Larch Interface Language for C.- 5.1 The relation between LCL and C.- 5.2 Function specifications.- 5.3 A guided tour through an LCL specification.- 6 LM3: A Larch Interface Language for Modula-3.- 6.1 The relation between LM3 and Modula-3.- 6.2 The LM3 semantic model.- 6.3 A guided tour through an LM3 specification.- 7 Using LP to Debug LSL Specifications.- 7.1 Semantic checks in LSL.- 7.2 Proof obligations for LSL specifications.- 7.3 Translating LSL traits into LP.- 7.4 Proof mechanisms in LP.- 7.5 Checking theory containment.- 7.6 Checking consistency.- 7.7 Extended example.- 7.8 Perspective.- 8 Conclusion.- A An LSL Handbook.- A.1 Introduction.- A.2 Foundations.- A.3 Integers.- A.4 Enumerations.- A.5 Containers.- A.6 Branching structures.- A.7 Maps.- A.8 Relations.- A.9 Graph theory.- A.10 Properties of single operators.- A.11 Properties of relational operators.- A.12 Orderings.- A.13 Lattice theory.- A.14 Group theory.- A.15 Number theory.- A.16 Floating point arithmetic.- B Implementations of Example LCL Interfaces.- C Lexical Forms and Initialization Files.- D Further Information and Tools.- E Classified Bibliography.- References.
Subject	:	Algebraische Spezifikation
Subject	:	LARCH
Subject	:	Softwareentwicklung
LC Classification	:	‭QA76.6‬‭J646 2012‬
Added Entry	:	James J Horning
	:	John V Guttag