stringtranslate.com

Subtipificación del comportamiento

En la programación orientada a objetos , la subtipificación conductual es el principio según el cual las subclases deben satisfacer las expectativas de los clientes que acceden a objetos de subclase a través de referencias del tipo de superclase, no solo en lo que respecta a la seguridad sintáctica (como la ausencia de errores de "método no encontrado") sino también en lo que respecta a la corrección conductual. En concreto, las propiedades que los clientes pueden demostrar utilizando la especificación del tipo presunto de un objeto deben cumplirse incluso aunque el objeto sea en realidad un miembro de un subtipo de ese tipo. [1]

Por ejemplo, considere un tipo Stack y un tipo Queue , que ambos tienen un método put para agregar un elemento y un método get para eliminar uno. Suponga que la documentación asociada con estos tipos especifica que los métodos del tipo Stack se comportarán como se espera para las pilas (es decir, exhibirán un comportamiento LIFO ), y que los métodos del tipo Queue se comportarán como se espera para las colas (es decir, exhibirán un comportamiento FIFO ). Supongamos, ahora, que el tipo Stack se declaró como una subclase del tipo Queue. La mayoría de los compiladores de lenguajes de programación ignoran la documentación y realizan solo las comprobaciones que son necesarias para preservar la seguridad de tipos . Dado que, para cada método del tipo Queue, el tipo Stack proporciona un método con un nombre y una firma coincidentes, esta comprobación tendría éxito. Sin embargo, los clientes que acceden a un objeto Stack a través de una referencia del tipo Queue esperarían, según la documentación de Queue, un comportamiento FIFO pero observarían un comportamiento LIFO, invalidando las pruebas de corrección de estos clientes y potencialmente conduciendo a un comportamiento incorrecto del programa en su conjunto.

Este ejemplo viola la subtipificación de comportamiento porque el tipo Stack no es un subtipo de comportamiento del tipo Queue: no es el caso de que el comportamiento descrito por la documentación del tipo Stack (es decir, el comportamiento LIFO) cumpla con la documentación del tipo Queue (que requiere el comportamiento FIFO).

Por el contrario, un programa en el que tanto Stack como Queue son subclases de un tipo Bag, cuya especificación para get es simplemente que elimina algún elemento, sí satisface la subtipificación conductual y permite a los clientes razonar con seguridad sobre la corrección en función de los tipos presuntos de los objetos con los que interactúan. De hecho, cualquier objeto que satisfaga la especificación Stack o Queue también satisface la especificación Bag.

Es importante destacar que si un tipo S es un subtipo conductual de un tipo T depende únicamente de la especificación (es decir, la documentación ) del tipo T; la implementación del tipo T, si tiene alguna, es completamente irrelevante para esta cuestión. De hecho, el tipo T ni siquiera necesita tener una implementación; podría ser una clase puramente abstracta. Como otro ejemplo, el tipo Stack anterior es un subtipo conductual del tipo Bag incluso si la implementación del tipo Bag muestra un comportamiento FIFO: lo que importa es que la especificación del tipo Bag no especifica qué elemento se elimina mediante el método get . Esto también significa que la subtipificación conductual se puede discutir solo con respecto a una especificación (conductual) particular para cada tipo involucrado y que si los tipos involucrados no tienen una especificación conductual bien definida, la subtipificación conductual no se puede discutir de manera significativa.

Verificación de subtipos de comportamiento

Un tipo S es un subtipo conductual de un tipo T si cada comportamiento permitido por la especificación de S también está permitido por la especificación de T. Esto requiere, en particular, que para cada método M de T, la especificación de M en S sea más fuerte que la de T.

Una especificación de método dada por una precondición P s y una postcondición Q s es más fuerte que una dada por una precondición P t y una postcondición Q t (formalmente: (P s , Q s ) ⇒ (P t , Q t )) si P s es más débil que P t (es decir, P t implica P s ) y Q s es más fuerte que Q t (es decir, Q s implica Q t ). Es decir, el fortalecimiento de una especificación de método se puede hacer fortaleciendo la postcondición y debilitando la precondición. De hecho, una especificación de método es más fuerte si impone restricciones más específicas en las salidas para las entradas que ya estaban soportadas, o si requiere que se soporten más entradas.

Por ejemplo, considere la especificación (muy débil) para un método que calcula el valor absoluto de un argumento x , que especifica una condición previa 0 ≤ x y una condición posterior 0 ≤ resultado. Esta especificación dice que el método no necesita admitir valores negativos para x , y solo necesita asegurar que el resultado también sea no negativo. Dos formas posibles de fortalecer esta especificación son fortaleciendo la condición posterior para indicar result = |x|, es decir, el resultado es igual al valor absoluto de x, o debilitando la condición previa a "verdadero", es decir, todos los valores para x deben ser admitidos. Por supuesto, también podemos combinar ambos, en una especificación que establezca que el resultado debe ser igual al valor absoluto de x , para cualquier valor de x .

Nótese, sin embargo, que es posible fortalecer una especificación ((P s , Q s ) ⇒ (P t , Q t )) sin fortalecer la postcondición (Q s ⇏ Q t ). [2] [3] Considérese una especificación para el método del valor absoluto que especifica una precondición 0 ≤ x y un resultado de postcondición = x. La especificación que especifica una precondición "verdadera" y un resultado de postcondición = |x| fortalece esta especificación, aunque el resultado de postcondición = |x| no fortalece (o debilite) el resultado de postcondición = x. La condición necesaria para que una especificación con precondición P s y postcondición Q s sea más fuerte que una especificación con precondición P t y postcondición Q t es que P s es más débil que P t y "Q s o no P s " es más fuerte que "Q t o no P t ". De hecho, "resultado = |x| o falso" fortalece "resultado = x o x < 0".

"Sustituibilidad"

En un influyente discurso de apertura [4] sobre abstracción de datos y jerarquías de clases en la conferencia de investigación de lenguajes de programación OOPSLA 1987, Barbara Liskov dijo lo siguiente: "Lo que se busca aquí es algo como la siguiente propiedad de sustitución: si para cada objeto de tipo S hay un objeto de tipo T tal que para todos los programas P definidos en términos de T, el comportamiento de P no cambia cuando se sustituye por , entonces S es un subtipo de T". Esta caracterización ha sido ampliamente conocida desde entonces como el Principio de Sustitución de Liskov (LSP) . Desafortunadamente, sin embargo, tiene varios problemas. En primer lugar, en su formulación original, es demasiado fuerte: rara vez queremos que el comportamiento de una subclase sea idéntico al de su superclase; la sustitución de un objeto de subclase por un objeto de superclase se hace a menudo con la intención de cambiar el comportamiento del programa, aunque, si se respeta la subtipificación del comportamiento, de una manera que mantenga las propiedades deseables del programa. En segundo lugar, no hace mención de especificaciones , por lo que invita a una lectura incorrecta donde la implementación del tipo S se compara con la implementación del tipo T. Esto es problemático por varias razones, una de ellas es que no admite el caso común donde T es abstracto y no tiene implementación. En tercer lugar, y de manera más sutil, en el contexto de la programación imperativa orientada a objetos es difícil definir con precisión lo que significa cuantificar universal o existencialmente sobre objetos de un tipo dado, o sustituir un objeto por otro. [3] En el ejemplo anterior, no estamos sustituyendo un objeto Stack por un objeto Bag, simplemente estamos usando un objeto Stack como un objeto Bag.

En una entrevista en 2016, la propia Liskov explica que lo que presentó en su discurso de apertura fue una "regla informal", que Jeannette Wing propuso más tarde que "trataran de averiguar exactamente qué significa esto", lo que llevó a su publicación conjunta [1] sobre subtipificación del comportamiento, y de hecho que "técnicamente, se llama subtipificación del comportamiento". [5] Durante la entrevista, no utiliza terminología de sustitución para discutir los conceptos.

Notas

  1. ^ ab Liskov, Barbara; Wing, Jeannette (1994-11-01). "Una noción conductual de subtipificación". ACM Transactions on Programming Languages ​​and Systems . 16 (6): 1811–1841. doi : 10.1145/197320.197383 .
  2. ^ Parkinson, Matthew J. (2005). Razonamiento local para Java (PDF) (PhD). Universidad de Cambridge.
  3. ^ ab Leavens, Gary T.; Naumann, David A. (agosto de 2015). "Subtipificación conductual, herencia de especificaciones y razonamiento modular". ACM Transactions on Programming Languages ​​and Systems . 37 (4). doi : 10.1145/2766446 .
  4. ^ Liskov, B. (mayo de 1988). "Discurso inaugural: abstracción y jerarquía de datos". Avisos SIGPLAN de la ACM . 23 (5): 17–34. doi : 10.1145/62139.62141 .
  5. ^ van Vleck, Tom (20 de abril de 2016). Entrevista con Barbara Liskov. ACM. Archivado desde el original el 21 de diciembre de 2021.

Referencias