¿Por qué el subtipo conductual no se puede decidir?

12
  

El trabajo de Liskov en esta área se centró en los subtipos de comportamiento, que además del tipo de sistema de seguridad descrito en este artículo también requiere que los subtipos conserven todos los invariantes garantizados por los supertipos en algún contrato. [3] Esta definición de subtipo es generalmente indecidible, por lo que no puede ser verificada por un verificador de tipos.

De: enlace

    
pregunta q126y 05.12.2015 - 13:04

2 respuestas

24

Sea el contrato de operación o de Type T que se detenga para todas las entradas. Ahora decida si la operación o del subtipo S <: T satisface ese contrato: acaba de resolver el Problema de detención .

Más generalmente, S::o debe calcular la misma función que T::o si S <: T . Decidir si dos programas computan la misma función se llama Function Problem y es equivalente a resolver el problema de detención.

En general, la decisión estática de cualquier propiedad de tiempo de ejecución no trivial es casi siempre equivalente al problema de detención.

    
respondido por el Jörg W Mittag 05.12.2015 - 13:11
12

Porque casi todas las preguntas sobre el comportamiento de los programas son indecibles. Por Teorema de Rice , cualquier problema de decisión de la forma:

  

Algunos programas calculan funciones que tienen esta propiedad, otros programas computan funciones que no tienen esta propiedad. Dado un programa P, ¿la función calculada por P tiene la propiedad mencionada o no?

es indecidible. Entonces, por ejemplo, no siempre se puede distinguir el código que calcula el cuadrado de una entrada del código que no lo hace. Aunque en casos simples, a menudo es posible probar que una función lo hace o no, no hay un procedimiento general que funcione para todos los programas.

Casi cualquier invariante de comportamiento interesante cae bajo el teorema de Rice, ya que esas afirmaciones rara vez (si alguna) hablan de cómo se ve el método internamente, solo lo que devuelve y los efectos secundarios que causa en respuesta a ciertas entradas.     

respondido por el user7043 05.12.2015 - 13:26

Lea otras preguntas en las etiquetas