PDF de programación - Semántica operacional - Tecnología de la Programación

Tecnología de la Programación

Semántica Operacional

David Cabrero Souto

Facultad de Informática
Universidade da Coruña

Curso 2007/2008

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal de propiedades .
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal de propiedades .
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal de propiedades .
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal de propiedades .
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal (base matemática) de propiedades .
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal (base matemática) de propiedades (para
todos los casos).
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Verificación formal

Recordar descriptores BOE:

Diseño de algoritmos
Análisis de algoritmos
Lenguajes de programación
Diseño de programas: Descomposición modular y
documentación
Técnicas de verificación
Pruebas de programas

Pruebas de programas: validación

Ejecución de un conjunto de tests generados sintética o
manualmente.

Prueba formal de propiedades: verificación

Demostración formal (base matemática) de propiedades (para
todos los casos).
Necesitamos una definición formal del significado (semántica)
de los lenguajes de programación.

Lenguaje de ejemplo

IMP (IMPerativo)
Estructuras básicas:

Secuencia
Alternativa
Repetición

Cambio de estado: variables y asignación.
Tipos básicos: enteros, strings.
Tipos compuestos: arrays.
Funciones.

IMP. Sintaxis aproximada

IMP ::= ’eof’

| CMDS ’eof’

CMDS ::= CMD ’;’

| CMD ’;’ CMDS

CMD ::= ’skip’

| Type Variable ’:=’ EXP
| Variable ’:=’ EXP
| Type Variable ’[’ Exp ’]’ ’:=’ EXP
| Variable ’[’ Exp ’]’ ’:=’ EXP
| ’if’ EXP ’then’ CMDS ’else’ CMDS ’fi’
| ’while’ EXP ’do’ CMDS ’done’
| ’print’ EXP

Semántica operacional

Define la semántica de un lenguaje de programación en
función de los cambios de estado que producen cada una de
las instrucciones del lenguaje.
No es adecuado para todo tipo de lenguajes.
El estado se representa mediante un modelo o abstracción.

IMP- Definición (I)

Conjuntos sintácticos asociados con IMP.

números N
Booleanos T = {true, false}
Posiciones de memoria Loc
Expresiones aritméticas Aexp
Expresiones booleanas Bexp
Comandos Com

IMP- Definición (I)

Conjuntos sintácticos asociados con IMP.

números N
Booleanos T = {true, false}
Posiciones de memoria Loc
Expresiones aritméticas Aexp
Expresiones booleanas Bexp
Comandos Com

IMP- Definición (I)

Conjuntos sintácticos asociados con IMP.

números N
Booleanos T = {true, false}
Posiciones de memoria Loc
Expresiones aritméticas Aexp
Expresiones booleanas Bexp
Comandos Com

IMP- Definición (I)

Conjuntos sintácticos asociados con IMP.

números N
Booleanos T = {true, false}
Posiciones de memoria Loc
Expresiones aritméticas Aexp
Expresiones booleanas Bexp
Comandos Com

IMP- Definición (I)

Conjuntos sintácticos asociados con IMP.

números N
Booleanos T = {true, false}
Posiciones de memoria Loc
Expresiones aritméticas Aexp
Expresiones booleanas Bexp
Comandos Com

IMP- Definición (I)

Conjuntos sintácticos asociados con IMP.

números N
Booleanos T = {true, false}
Posiciones de memoria Loc
Expresiones aritméticas Aexp
Expresiones booleanas Bexp
Comandos Com

IMP- Definición (II)

Convenciones

n, m son variables en N
X , Y son variables en Loc
ai son variables en Aexp
bi son variables en Bexp
ci son variables en Com

n, m ∈ N
X , Y ∈ Loc
ai ∈ Aexp
bi ∈ Bexp
ci ∈ Com

IMP- Definición (II)

Convenciones

n, m son variables en N
X , Y son variables en Loc
ai son variables en Aexp
bi son variables en Bexp
ci son variables en Com

n, m ∈ N
X , Y ∈ Loc
ai ∈ Aexp
bi ∈ Bexp
ci ∈ Com

IMP- Definición (II)

Convenciones

n, m son variables en N
X , Y son variables en Loc
ai son variables en Aexp
bi son variables en Bexp
ci son variables en Com

n, m ∈ N
X , Y ∈ Loc
ai ∈ Aexp
bi ∈ Bexp
ci ∈ Com

IMP- Definición (II)

Convenciones

n, m son variables en N
X , Y son variables en Loc
ai son variables en Aexp
bi son variables en Bexp
ci son variables en Com

n, m ∈ N
X , Y ∈ Loc
ai ∈ Aexp
bi ∈ Bexp
ci ∈ Com

IMP- Definición (II)

Convenciones

n, m son variables en N
X , Y son variables en Loc
ai son variables en Aexp
bi son variables en Bexp
ci son variables en Com

n, m ∈ N
X , Y ∈ Loc
ai ∈ Aexp
bi ∈ Bexp
ci ∈ Com

IMP- Definición (Aexp)

Expresiones aritméticas
Aexp

::= n
|
X
|
a0 + a1
|
a0 − a1
|
a0 ∗ a1

IMP- Definición (Bexp)

Expresiones booleanas
Bexp

::= true
|
false
|
a0 = a1
|
a0 <= a1
|
not b
|
b0 and b1
|
b0 or b1

IMP- Definición (Comm)

Instrucciones
Comm ::= skip
|
|
|
| while b do c done

X := a
c0; c1
if b then c0 else c1 fi

Estados

El conjunto de estados Σ está formado por las funciones:

σ : Loc− > N

(Sólo variables enteras)
Dado un estado σ, representaremos el valor de la posicion X
como:

σ(X )



Y la extensión de un estado σ[X ← m]:

σ[X ← m](Y ) =

Indistintamente

σ[X ← m]

m
Y = X ,
σ(Y ) si Y = X .
ó

σ[m/X ]

Evaluación

Evaluación de una expresión aritmética a en un estado σ

< a, σ >→ n

Evaluación de una expresión booleana b en un estado σ

< b, σ >→ {true, false}

Ejecución de una instrucción c en un estado σ

< c, σ >→ σ

Secuentes

Si las premisas son ciertas, se puede deducir la conclusión.

< premisas >
< conclusion >
F1 . . . Fn → G1 . . . Gm

F1 . . . Fn
G1 . . . Gm
Las usaremos para definir la semántica operacional.

Evaluación de expresiones aritméticas

Constantes

Variables

Suma

Resta

Multiplicación

< n, σ >→ n

< X , σ >→ σ(X )

< a0, σ >→ n < a1, σ >→ m

< a0 + a1, σ >→ n + m

< a0, σ >→ n < a1, σ >→ m

< a0 − a1, σ >→ n − m

< a0, σ >→ n < a1, σ >→ m

< a0 ∗ a1, σ >→ n ∗ m

Evaluación de expresiones aritméticas

Constantes

Variables

Suma

Resta

Multiplicación

< n, σ >→ n

< X , σ >→ σ(X )

< a0, σ >→ n < a1, σ >→ m

< a0 + a1, σ >→ n + m

< a0, σ >→ n < a1, σ >→ m

< a0 − a1, σ >→ n − m

< a0, σ >→ n < a1, σ >→ m

< a0 ∗ a1, σ >→ n ∗ m

Evaluación de expresiones aritméticas

Constantes

Variables

Suma

Resta

Multiplicación

< n, σ >→ n

< X , σ >→ σ(X )

< a0, σ >→ n < a1, σ >→ m

< a0 + a1, σ >→ n + m

< a0, σ >→ n < a1, σ >→ m

< a0 − a1, σ >→ n − m

< a0, σ >→ n < a1, σ >→ m

< a0 ∗ a1, σ >→ n ∗ m

Evaluación de expresiones aritméticas

Constantes

Variables

Suma

Resta

Multiplicación

< n, σ >→ n

< X , σ >→ σ(X )

< a0, σ >→ n < a1, σ >→ m

< a0 + a1, σ >→ n + m

< a0, σ >→ n < a1, σ >→ m

< a0 − a1, σ >→ n − m

< a0, σ >→ n < a1, σ >→ m

< a0 ∗ a1, σ >→ n ∗ m

Evaluación de expresiones aritméticas

Constantes

Variables

Suma

Resta

Multiplicación

< n, σ >→ n

< X , σ >→ σ(X )

< a0, σ >→ n < a1, σ >→ m

< a0 + a1, σ >→ n + m

< a0, σ >→ n < a1, σ >→ m

< a0 − a1, σ >→ n − m

< a0, σ >→ n < a1, σ >→ m

< a0 ∗ a1, σ >→ n ∗ m

Evaluación de expresiones booleanas (I)

Constantes

< true, σ >→ true
Comparación aritmética

< false, σ >→ false

< a0, σ >→ n < a1, σ >→ m
< a0, σ >→ n < a1, σ >→ m

< a0 = a1, σ >→ true
< a0 = a1, σ >→ false

< a0, σ >→ n < a1, σ >→ m
< a0 <= a1, σ >→ true
< a0, σ >→ n < a1, σ >→ m
< a0 <= a1, σ >→ false

n = m
n = m

n <= m

n > m

Evaluación de expresiones booleanas (I)

Constantes

< true, σ >→ true
Comparación aritmética

< false, σ >→ false

< a0, σ >→ n < a1, σ >→ m
< a0, σ >→ n < a1, σ >→ m

< a0 = a1, σ >→ true
< a0 = a1, σ >→ false

< a0, σ >→ n < a1, σ >→ m
< a0 <= a1, σ >→ true
< a0, σ >→ n < a1, σ >→ m
< a0 <= a1, σ >→ false

n = m
n = m

n <= m

n > m

Evaluación de expresiones booleanas (II)

Negación