Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Algebraic Methodology and Software Technology [[electronic resource] ] : 5th International Conference, AMAST '96 Munich, Germany, July 1996. Proceedings / / edited by Martin Wirsing, Maurice Nivat
| Algebraic Methodology and Software Technology [[electronic resource] ] : 5th International Conference, AMAST '96 Munich, Germany, July 1996. Proceedings / / edited by Martin Wirsing, Maurice Nivat |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (XIII, 647 p.) |
| Disciplina | 005.1/2/015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Software engineering Computer logic Mathematical logic Special purpose computers Theory of Computation Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Mathematical Logic and Formal Languages Software Engineering Special Purpose and Application-Based Systems |
| ISBN | 3-540-68595-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Two industrial trials of formal specification -- Industrial applications of ASF+SDF -- The embedded software of an electricity meter: An experience in using formal methods in an industrial project -- Applying research results in the industrial environment: The case of the TRIO specification language -- Using heterogeneous formal methods in distributed software engineering education -- Introducing formal methods to software engineers through OMG's CORBA environment and interface definition language -- Toward a classification approach to design -- Semantic foundations for embedding HOL in Nuprl -- Free variable tableaux for a many sorted logic with preorders -- Automating induction over mutually recursive functions -- Pushouts of order-sorted algebraic specifications -- A formal framework for modules with state -- Object-oriented implementation of abstract data type specifications -- On the completeness of the equations for the Kleene star in bisimulation -- An equational axiomatization of observation congruence for prefix iteration -- Finite axiom systems for testing preorder and De Simone process languages -- Constructive semantics of Esterel: From theory to practice (abstract) -- Using ghost variables to prove refinement -- Tracing the origins of verification conditions -- Preprocessing for invariant validation -- Formal verification of Signal programs: Application to a power transformer station controller -- The discrete time toolbus -- A study on the specification and verification of performance properties -- Symbolic bisimulation for timed processes -- Approximative analysis by process algebra with graded spatial actions -- Boolean formalism and explanations -- Proving existential termination of normal logic programs -- Programming in Lygon: An overview -- Some characteristics of strong innermost normalization -- On the emergence of properties in component-based systems -- Algebraic view specification -- Towards heterogeneous formal specifications -- A categorical characterization of consistency results -- Algebraic specification of reactive systems -- A model for mobile point-to-point data-flow networks without channel sharing -- Coalgebraic specifications and models of deterministic hybrid systems -- A bounded retransmission protocol for large data packets -- SPECWARE: An advanced environment for the formal development of complex software systems -- Asspegique+ an integrated specification environment providing inter-operability of tools -- Towards integrating algebraic specification and functional programming: the Opal system -- InterACT: An interactive theorem prover for algebraic specifications -- A new proof-manager and graphic interface for the Larch Prover -- TERSE: A visual environment for supporting analysis, verification and transformation of term rewriting systems -- The ToolBus coordination architecture -- ASD: The action semantic description tools -- Using occurrrence and evolving algebras for the specification of language-based programming tools -- ECHIDNA: A system for manipulating explicit choice higher dimensional automata -- Verification using PEP -- The Fc2tools set -- Programming in Lygon: A system demonstration -- CtCoq: A system presentation -- The Typelab specification and verification environment -- Incremental formalization -- Proplane: A specification development environment -- A logic-based technology to mechanize software components reuse -- TkGofer: A functional GUI library -- ALPHA — A class library for a metamodel based on algebraic graph theory -- Resolution of goals with the functional and logic programming language LPG: Impact of abstract interpretation -- Combining reductions and computations in ReDuX -- Conditional directed narrowing. |
| Record Nr. | UNISA-996465664103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
The B Language and Method [[electronic resource] ] : A Guide to Practical Formal Development / / by Kevin Lano
| The B Language and Method [[electronic resource] ] : A Guide to Practical Formal Development / / by Kevin Lano |
| Autore | Lano Kevin |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | London : , : Springer London : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (VIII, 232 p.) |
| Disciplina | 005.1/2/015113 |
| Collana | Formal Approaches to Computing and Information Technology (FACIT) |
| Soggetto topico |
Software engineering
Mathematical logic Programming languages (Electronic computers) Software Engineering Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters |
| ISBN | 1-4471-1494-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1 Introduction -- 1.1 Formal Methods -- 1.2 The History of B -- 1.3 The Relationship of B to Other Formal Methods -- 1.4 Summary -- 2 The Foundations of B AMN -- 2.1 Mathematical Notation -- 2.2 Defining Operations -- 2.3 Abstract Machines -- 2.4 Machine Composition Mechanisms -- 2.5 Refinement -- 2.6 Implementation -- 2.7 Summary -- 2.8 Exercises 1 -- 3 Analysis and Specification -- 3.1 Requirements Analysis -- 3.2 Specification Development -- 3.3 Animation -- 3.4 Proof of Internal Consistency Obligations -- 3.5 Ship Loading Case Study — Specification -- 3.6 Renaming -- 3.7 Aggregation -- 3.8 Summary -- 3.9 Exercises 2 -- 4 Design and Implementation -- 4.1 The Layered Development Paradigm -- 4.2 Refinement Examples -- 4.3 Proofs of Refinement -- 4.4 Decomposing Implementations -- 4.5 Ship Loading Case Study — Implementation -- 4.6 Summary -- 4.7 Exercises 3 -- 5 Case Studies -- 5.1 Personnel System Development -- 5.2 Mine Pump Control -- 5.3 Vending Machine -- 6 Conclusions -- A Exercise Solutions -- A.1 Exercises 1 -- A.2 Exercises 2 -- A.3 Exercises 3 -- B Properties of Weakest Preconditions -- B.1 Termination and Feasibility -- B.2 Set-theoretic Semantics -- B.3 Refinement -- B.4 Well-formedness Obligations -- B.5 Normal Forms -- B.6 Rules for ? -- B.7 Definition of := -- C Proof Techniques. |
| Record Nr. | UNINA-9910480198303321 |
Lano Kevin
|
||
| London : , : Springer London : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The B Language and Method [[electronic resource] ] : A Guide to Practical Formal Development / / by Kevin Lano
| The B Language and Method [[electronic resource] ] : A Guide to Practical Formal Development / / by Kevin Lano |
| Autore | Lano Kevin |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | London : , : Springer London : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (VIII, 232 p.) |
| Disciplina | 005.1/2/015113 |
| Collana | Formal Approaches to Computing and Information Technology (FACIT) |
| Soggetto topico |
Software engineering
Mathematical logic Programming languages (Electronic computers) Software Engineering Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters |
| ISBN | 1-4471-1494-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1 Introduction -- 1.1 Formal Methods -- 1.2 The History of B -- 1.3 The Relationship of B to Other Formal Methods -- 1.4 Summary -- 2 The Foundations of B AMN -- 2.1 Mathematical Notation -- 2.2 Defining Operations -- 2.3 Abstract Machines -- 2.4 Machine Composition Mechanisms -- 2.5 Refinement -- 2.6 Implementation -- 2.7 Summary -- 2.8 Exercises 1 -- 3 Analysis and Specification -- 3.1 Requirements Analysis -- 3.2 Specification Development -- 3.3 Animation -- 3.4 Proof of Internal Consistency Obligations -- 3.5 Ship Loading Case Study — Specification -- 3.6 Renaming -- 3.7 Aggregation -- 3.8 Summary -- 3.9 Exercises 2 -- 4 Design and Implementation -- 4.1 The Layered Development Paradigm -- 4.2 Refinement Examples -- 4.3 Proofs of Refinement -- 4.4 Decomposing Implementations -- 4.5 Ship Loading Case Study — Implementation -- 4.6 Summary -- 4.7 Exercises 3 -- 5 Case Studies -- 5.1 Personnel System Development -- 5.2 Mine Pump Control -- 5.3 Vending Machine -- 6 Conclusions -- A Exercise Solutions -- A.1 Exercises 1 -- A.2 Exercises 2 -- A.3 Exercises 3 -- B Properties of Weakest Preconditions -- B.1 Termination and Feasibility -- B.2 Set-theoretic Semantics -- B.3 Refinement -- B.4 Well-formedness Obligations -- B.5 Normal Forms -- B.6 Rules for ? -- B.7 Definition of := -- C Proof Techniques. |
| Record Nr. | UNINA-9910789343303321 |
|
Lano Kevin
|
||
| London : , : Springer London : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The B Language and Method : A Guide to Practical Formal Development / / by Kevin Lano
| The B Language and Method : A Guide to Practical Formal Development / / by Kevin Lano |
| Autore | Lano Kevin |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | London : , : Springer London : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (VIII, 232 p.) |
| Disciplina | 005.1/2/015113 |
| Collana | Formal Approaches to Computing and Information Technology (FACIT) |
| Soggetto topico |
Software engineering
Mathematical logic Programming languages (Electronic computers) Software Engineering Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters |
| ISBN | 1-4471-1494-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1 Introduction -- 1.1 Formal Methods -- 1.2 The History of B -- 1.3 The Relationship of B to Other Formal Methods -- 1.4 Summary -- 2 The Foundations of B AMN -- 2.1 Mathematical Notation -- 2.2 Defining Operations -- 2.3 Abstract Machines -- 2.4 Machine Composition Mechanisms -- 2.5 Refinement -- 2.6 Implementation -- 2.7 Summary -- 2.8 Exercises 1 -- 3 Analysis and Specification -- 3.1 Requirements Analysis -- 3.2 Specification Development -- 3.3 Animation -- 3.4 Proof of Internal Consistency Obligations -- 3.5 Ship Loading Case Study — Specification -- 3.6 Renaming -- 3.7 Aggregation -- 3.8 Summary -- 3.9 Exercises 2 -- 4 Design and Implementation -- 4.1 The Layered Development Paradigm -- 4.2 Refinement Examples -- 4.3 Proofs of Refinement -- 4.4 Decomposing Implementations -- 4.5 Ship Loading Case Study — Implementation -- 4.6 Summary -- 4.7 Exercises 3 -- 5 Case Studies -- 5.1 Personnel System Development -- 5.2 Mine Pump Control -- 5.3 Vending Machine -- 6 Conclusions -- A Exercise Solutions -- A.1 Exercises 1 -- A.2 Exercises 2 -- A.3 Exercises 3 -- B Properties of Weakest Preconditions -- B.1 Termination and Feasibility -- B.2 Set-theoretic Semantics -- B.3 Refinement -- B.4 Well-formedness Obligations -- B.5 Normal Forms -- B.6 Rules for ? -- B.7 Definition of := -- C Proof Techniques. |
| Record Nr. | UNINA-9910828902403321 |
|
Lano Kevin
|
||
| London : , : Springer London : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||