Principe de substitution de Liskov

Résumé

vignette|Barbara Liskov en 2010 Le principe de substitution de Liskov (LSP) est, en programmation orientée objet, une définition particulière de la notion de sous-type. Il a été formulé par Barbara Liskov et Jeannette Wing dans un article intitulé Family Values: A Behavioral Notion of Subtyping : Liskov et Wing en ont proposé la formulation condensée suivante : :Si q(x) est une propriété démontrable pour tout objet x de type T, alors q(y) est vraie pour tout objet y de type S tel que S est un sous-type de T. Principe La notion de sous-type telle que définie par Liskov et Wing est fondée sur la notion de substituabilité : si S est un sous-type de T, alors tout objet de type T peut être remplacé par un objet de type S sans altérer les propriétés désirables du programme concerné. Le principe de Liskov impose des restrict

Source officielle

https://fr.wikipedia.org/wiki/Principe_de_substitution_de_Liskov

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (5)

Publications associées

Chargement

Personnes associées

Aucun résultat

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés (12)

Concepts associés

Chargement

Cours associés (6)

Cours associés

Chargement

Séances de cours associées (8)

Afficher plus

Séances de cours associées

Chargement

In this thesis we address the problem of safe substitutability in mobile component-oriented formalisms. We try to give a solution for different definitions of "safe" through a new notion of subtyping based on flexibility and observation. The aim is to have a definition which is applicable to a large numbers of existing formalisms, and which itself may be seen as an abstraction of many existing definitions of subtyping. In a similar way, we also try to see the verification of such relations in a way that may be applicable to many formalisms, and which may be seen as "containing" many existing techniques. Our hope is that our work may link these subtype definitions or verification techniques to formalisms they were not originally designed for. The contribution of this thesis can be divided in several points. First of all, the full formal definition of a "descriptive" component-oriented formalism based on concurrency, non determinism, complex composition and mobility. Also, the definition of a general flexible notion of subtyping, as well as a more particular example. Verification techniques for these subtyping relations are also grouped under the concept of component transformation, which is shown to include many other works. Finally, to illustrate the main concepts of our work, we provide a case study with a model of a "mobile" drinks dispenser.

EPFL2004

Chargement

Towards the Formal Integration of Two Upcoming Standards: IEC61970 and IEC61850

Christian Frei, Tatjana Kostic, Otto Preiss

AbstractThe constant demand for a better integration of utility applications and systems provokes the question on the compatibility of standards that were, and still are, developed for these individual utility disciplines. This paper discusses the need for an integration of two particularly important emerging standards related to data interchange in substations (IEC 61850) and control centres (IEC 61970). The relatively independent development of these two standards motivated us to create a model that can show explicitly how concepts from one standard relate to those of the other. Further, by making these models formal, which at least in the case of IEC 61850 is absent in its current daft, we can show the benefits in checking internal model consistency and in automating the model mapping. Concretely, our UML models proved helpful in detecting inconsistencies in draft versions of the IEC 61850 and they served as a basis for the software tool-based, bi-directional mapping of IEC 61850 to IEC 61970 data representations.

2003

Chargement

Type Soundness Proofs with Definitional Interpreters

Nada Amin, Tiark Rompf

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculus, cannot simultaneously support key metatheoretic properties such as environment narrowing and subtyping transitivity, which are usually required for a type soundness proof. Moreover, Scala and many other realistic languages lack a general substitution property. The first contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proofs in this style for System F

Assoc Computing Machinery2017

Chargement