Análisis lógico Lenguajes de programación

Programación imperativa Programación funcional Concurrencia

Análisis lógicoLenguajes de programación

Francisco Hernández Quiroz

Departamento de MatemáticasFacultad de Ciencias, UNAME-mail: [email protected]

Página Web: www.matematicas.unam.mx/fhq

25 de marzo de 2010



Lenguajes de programación

Con el fin de ilustrar algunas aplicaciones de la lógica a lacomputación, presentaremos tres tipos de lenguajes:

Dos lenguajes imperativos: IMP y el lenguaje de comandoscustodiados de Dijkstra.

Dos lenguajes funcionales. La sintaxis de los dos es igual y sedistinguen únicamente por su semántica.

Un lenguaje de descripción de procesos concurrentes: Calculusof Concurrent Systems, el cual más abstracto que un lenguaje deprogramación en sentido estricto.



Sintaxis y semántica formales

La notación de Backus-Naur (BNF) es ya un estándar para lapresentación de la sintaxis de lenguajes de programación.

Sin embargo, en el terreno de la semántica siguenpredominando las explicaciones informales.

Aquí se usará una notación formal: la semántica operacionalestructural.

Aunque no es el único formalismo para describir los lenguajesde programación (por ejemplo, la semántica denotacional es unaopción matemáticamente más elegante) sí es el más cercano alas intuiciones del programador típico.


Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo

Lenguaje IMP

La sintaxis del lenguaje IMP se describe a continuación en la notaciónde Backus-Naur. Empezaremos con las expresiones aritméticas EA:

A ::= n | X | (A + A′) | (A− A′) | (A× A′)

donde n ∈ Z, X ∈ Loc y A, A′ ∈ EA.Tenemos ahora las expresiones booleanas EB:

B ::= V | F | (A = A′) | (A ≤ A′) | ¬B | (B ∧ B′) | (B ∨ B′)

donde A, A′ ∈ EA y B, B′ ∈ EB.Finalmente, los comandos del lenguaje IMP se definen así:

C ::= skip | X := A | (C ; C′) | (if B then C else C′) | (while B do C)

donde A ∈ EA, B ∈ EB y C, C′ ∈ IMP.



Semántica operacional estructural I

La forma más común de definir el significado de lasconstrucciones de un lenguaje es por medio de explicaciones enuna lengua natural (inglés, generalmente).

Sin embargo, el lenguaje natural se presta a las ambigüedades yéstas, a los errores o a las divergencias entre las diferentesimplementaciones de un mismo lenguaje.

Para evitar estos problemas, aquí se usarán reglas de semánticaoperacional estructural o SOE, para abreviar.

Una regla de inferencia tiene la forma siguiente:

p1, . . . , pn

q

donde p1, . . . , pn son las premisas y q es la conclusión.



Semántica operacional estructural II

Las reglas de SOE son un tipo particular de reglas de inferenciaen las que las premisas y la conclusión son transiciones.

Una transición tiene la forma

α→ β

La forma concreta de las expresiones α y β, así como lastransiciones aceptables, se definirán más adelante.



¿Qué es la programación imperativa?

IMP es un lenguaje imperativo típico: el comando básico es laasignación de valor a las localidades de la memoria de lacomputadora.

Para definir el significado de una asignación se parte de laexistencia de una máquina virtual que posee una memoria conlocalidades con nombre:

Loc = {X, Y , Z, X0, . . . }

Las localidades pueden tomar valores de Z.



Estados de la memoria

Un estado de la memoria es una función σ : Loc→ Z.La expresión

σ(X)

nos dice qué valor contiene la localidad x en el estado σ.La alteración del valor de una sola localidad de la memoriacuando se encuentra en el estado σ se representa con la función

σ[m/X],

donde X es la localidad modificada y m es el nuevo valor.Formalmente:

σ[m/X](Y) =

{σ(Y) si X 6= Y

m en caso contrario.

El conjunto de estados es Σ.



SOE para IMP. Expresiones aritméticas

En el caso de las expresiones aritméticas, las transiciones α→ βtiene la forma

〈a,σ〉 → n

donde a ∈ EA, σ ∈ Σ y n ∈ Z.Diremos que “evaluar operacionalmente la expresión a en el estadoσ da como resultado el valor n”.Dicha evaluación se realiza de acuerdo con las siguientes reglas:

〈n,σ〉 → n 〈x,σ〉 → σ(X)

〈a0,σ〉 → n0 〈a1,σ〉 → n1 n0 op n1 = n〈a0 op a1,σ〉 → n

En esta regla op puede ser +, − o × y op, +Z, −Z o ×Z (ambosoperadores deben coincidir).



SOE para IMP. Expresiones booleanas I

En las expresiones booleanas, una transición es 〈b,σ〉 → T, conb ∈ EB, σ ∈ Σ y T ∈ {V, F}. Las reglas operacionales son:

〈V,σ〉 → V 〈F,σ〉 → F

〈a0,σ〉 → n 〈a1,σ〉 → m〈a0 = a1,σ〉 → V

sii n y m son iguales

〈a0,σ〉 → n 〈a1,σ〉 → m〈a0 = a1,σ〉 → F

sii n y m no son iguales

〈a0,σ〉 → n 〈a1,σ〉 → m〈a0 ≤ a1,σ〉 → V

sii n es menor o igual a m

〈a0,σ〉 → n 〈a1,σ〉 → m〈a0 ≤ a1,σ〉 → F

sii n no es menor o igual a m



SOE para IMP. Expresiones booleanas II

〈b,σ〉 → V〈¬b,σ〉 → F

〈b,σ〉 → F〈¬b,σ〉 → V

〈b0,σ〉 → T0 〈b1,σ〉 → T1

〈b0 ∧ b1,σ〉 → Tcon T = V si T0, T1 = Vy T = F en caso contrario

〈b0,σ〉 → T0 〈b1,σ〉 → T1

〈b0 ∧ b1,σ〉 → Tcon T = V si T0 = V o T1 = Vy T = F en caso contrario



SOE para IMP. Comandos I

Las reglas de transición de los comandos son así:

〈c,σ〉 → σ′,

donde c ∈ IMP y σ, σ′ ∈ Σ.El valor de σ′ se infiere de este modo:

Comandos atómicos

〈skip,σ〉 → σ〈a,σ〉 → m

〈X := a,σ〉 → σ[m/X]

Composición secuencial

〈c0,σ〉 → σ′′ 〈c1,σ′′〉 → σ′

〈c0 ; c1,σ〉 → σ′



SOE para IMP. Comandos II

Condicionales

〈b,σ〉 → V 〈c0,σ〉 → σ′

〈if b then c0 else c1,σ〉 → σ′〈b,σ〉 → F 〈c1,σ〉 → σ′

〈if b then c0 else c1,σ〉 → σ′

Ciclos

〈b,σ〉 → F〈while b do c,σ〉 → σ

〈b,σ〉 → V 〈c,σ〉 → σ′′ 〈while b do c,σ′′〉 → σ′

〈while b do c,σ〉 → σ′



Ejemplo

Dadas las reglas anteriores, no es difícil ver que el programa de IMP

siguiente calcula el factorial del número n (si n ≥ 0) y lo guarda en lalocalidad Y :

X := 1;Y := 1;while X ≤ n do

(X := X + 1;Y := Y × X)



No determinismo

Como primera aproximación a la computación, IMP es bastantebueno. No obstante, hay una serie de “fenómenos”computacionales que no pueden modelarse con IMP.

Uno de estos es el no determinismo: la posibilidad de que laejecución de un programa dé resultados distintos en distintasocasiones a pesar de que recibe los mismos datos de entradasiempre.

El no determinismo puede surgir en diversas situaciones. La máscomún es la concurrencia de procesos, pero también puedepresentarse por una decisión en el diseño mismo de loslenguajes de programación.



Un lenguaje no determinista

Ahora se presentará un lenguaje imperativo con no determinismoexplícito. Para esto necesitaremos una categoría especial decomandos llamados comandos resguardados (guarded commands):

G ::= (B→ C) | (G G′)

donde G y G′ son comandos resguardados y B ∈ EB.Como los comandos resguardados son básicos en nuestro lenguaje,lo llamaremos GCL: guarded command language.He aquí la sintaxis de GCL:

C ::= skip | abort | X := A | (C ; C′) | if g fi | do g od

donde abort es un nuevo programa primitivo, G es un comandoresguardado y C, C′ ∈ GCL.



Semántica operacional I

Comencemos con las reglas de comandos resguardados:

〈b,σ〉 → V〈b→ c,σ〉 → 〈c,σ〉

〈b,σ〉 → F〈b→ c,σ〉 → fail

〈g0,σ〉 → 〈c,σ′〉〈g0 g1,σ〉 → 〈c,σ′〉

〈g1,σ〉 → 〈c,σ′〉〈g0 g1,σ〉 → 〈c,σ′〉

〈g0,σ〉 → fail 〈g1,σ〉 → fail〈g0 g1,σ〉 → fail



Semántica operacional I

Ahora seguimos con las reglas para comandos generales:

〈skip,σ〉 → σ〈a,σ〉 → m

〈X := a,σ〉 → σ[m/X]

〈c0,σ〉 → σ′′ 〈c1,σ′′〉 → σ′

〈c0 ; c1,σ〉 → σ′〈c0,σ〉 → 〈c′0,σ′〉

〈c0 ; c1,σ〉 → 〈c′0 ; c1,σ′〉

〈g,σ〉 → 〈c,σ′〉〈if g fi,σ〉 → 〈c,σ′〉

〈g,σ〉 → fail〈do g od,σ〉 → σ

〈g,σ〉 → 〈c,σ′〉〈do g od,σ〉 → 〈c ; do g od,σ′〉



Ejemplo

El lector puede verificar, haciendo uso de las reglas anteriores y de suconocimiento del , queEl siguiente programa implementa el viejo algoritmo de Euclides paracalcular el máximo común divisor de los enteros positivos n y m. Elresultado queda guardado en las localidades X y Y .

X := n;Y := m;do

X > Y → X := X − YY > X → Y := Y − X

odNota: X > Y es una abreviatura, obviamente, de Y ≤ X ∧ ¬(X = Y).


Programación imperativa Programación funcional Concurrencia Sintaxis Semánticas Ejemplos

Programación funcional

Un estilo de programación radicalmente distinto al imperativoes el funcional.

La idea básica es que en lugar de programas con instruccionesdetalladas para la computadora, se deben usar definiciones defunciones.

La ejecución de un programa consiste en la evaluación de unafunción definida anteriormente con argumentos concretos.



Sintaxis

Nuevamente, usaremos la notación Backus-Naur:

t ::= n | x | t + t′ | t− t′ | t× t′ | if t then t′ else t′′ | fi(t1, . . . , tn)

t, t′ y t′ designan términos del lenguaje funcional.

Obsérvese como en el condicional no se usan expresionesbooleanas sino términos como condición.

El valor 0 tendrá el papel de verdadero y cualquier otro valor seconsiderará falso.



Declaraciones

El estilo funcional de programación permite prescindir de lareferencia a una máquina virtual y su memoria.

Las funciones tomarán su significado a partir de declaraciones.

Una declaración es un conjunto finito de ecuaciones. Del ladoizquierdo aparece una función con variables como argumentos;del derecho, aparecen términos del lenguaje funcional.

f1(x1, . . . , xn1) = d1...

fk(x1, . . . , xnk) = dk

donde d1, . . . , dk son términos del lenguaje funcional.

No se permite más de una ecuación por cada función, pero sí seacepta la recursividad.



Semántica operacional

Las transiciones ahora son de la forma

t→ds t′

donde t y t′ son términos del lenguaje, d es una declaración y spuede tomar el valor v (llamada por valor) o n (llamada pornombre).

Las transiciones dependen de declaraciones específicas.

En el estilo de llamada por valor, los argumentos de las funcionesson evaluados antes de evaluar la función misma.

En el estilo de llamado por nombre, la evaluación se posponehasta que se evalúa el cuerpo mismo de la función.

La diferencia entre los dos estilos se manifiestan sólo en unaregla de evaluación de términos.



Semántica con llamada por valor

Números n→dv n Operadores

t0 →dv n0 t1 →d

v n1

t0 op t1 →dv n0 op n1

Condicional verdadero

t0 →dv 0 t1 →d

v n1

if t0 then t1 else t2 →dv n1

Condicional falso

t0 →dv n0 t2 →d

v n2 n0 6= 0if t0 then t1 else t2 →d

v n2

Funciones

t1 →dv n1 · · · tmi →d

v nmi di[n1/x1,...,nmi/xmi ]→d

v n

fi(t1, . . . , tmi)→dv n

Conviene prestar atención a la última regla, pues es la que varía conrespecto a la llamada por nombre.



Llamada por nombre

Números n→dn n Operadores

t0 →dn n0 t1 →d

n n1

t0 op t1 →dn n0 op n1

Condicional verdadero

t0 →dn 0 t1 →d

n n1

if t0 then t1 else t2 →dn n1

Condicional falso

t0 →dn n0 t2 →d

n n2 n0 6= 0if t0 then t1 else t2 →d

n n2

Funciones

di[t1/x1,...,tmi/xmi ]→d

n n

fi(t1, . . . , tmi)→dn n



Ejemplos I

Supóngase que se tiene la siguiente declaración:

f1(x) = if x then 1 else f1(x − 1)× xf2(x, y) = x

f3(x) = f3(x + 1)

Entonces el programa f1(n) calcula el factorial de n, encualquiera de los dos estilos de programación.En cambio, considérese el programa

f2(2, f3(1)).

De acuerdo con las reglas de llamado por nombre, para realizarla evaluación del programa debemos evaluar la expresión

x[x/2,y/f3(1)] = 2

que, de acuerdo con la regla para números, nos da 2.Francisco Hernández Quiroz


Ejemplos II

En cambio, las reglas de llamada por valor nos piden queprimero evaluemos los términos

2 y f3(1)

el segundo de los cuales nunca nos da un resultado, como sepuede deducir de la tercera ecuación de la declaración.

Nota

Si se adopta el estilo de llamada por valor, el lenguaje funcionalse asemeja a un subconjunto de ML.

Si se adopta llamada por nombre, será parecido a unsubconjunto de Haskell.


Programación imperativa Programación funcional Concurrencia Sintaxis Semántica Ejemplos

Concurrencia

La idea de que un sistema de cómputo se basa en la ejecuciónsecuencial de una serie de instrucciones por parte de un enteaislado hace mucho que es obsoleta.

La mayoría de los sistemas actuales contiene subsistemas queactúan de manera simultánea y que intercambian informaciónentre sí. Estos sistemas se llaman concurrentes.Hay varios modelos de cómo se realiza el intercambio deinformación entre subsistemas, pero dos son los fundamentales:

1 memoria compartida;2 envío de mensajes.

En el primero, hay un área de la memoria (variables, buffers,etc.) a la que varios sistemas concurrentes tienen acceso paraguardar o leer datos.

Por su parte, el envío de mensajes se realiza por un medioabierto (difusión) o por medio de canales específicos.



Communicating Concurrent Systems

En los 80, Robin Milner propuso un lenguaje de especificación paraprocesos concurrentes: CCS (Communicating Concurrent Systems).Dicho lenguaje consta de:

Un conjunto de valores (enteros, por ejemplo) que se envían oreciben a través de canales α, β, etc.

Operadores para la composición secuencial o paralela deprocesos.

Un operador de “elección”

Operaciones para reetiquetar canales y restringir el acceso aéstos.



Sintaxis I

Para comenzar, las acciones básicas de comunicación entre procesos:

λ ::= τ | α!m | α?m

τ es la acción nula, α!m es el envío de m por el puerto de salida delcanal α y α?m es la recepción de m por el puerto de entrada delmismo canal.Los procesos de CCS se definen así:

p ::= nil | λ . p |∑i∈I

pi | p ‖ p′ | p\L | p[f ] | P

En términos informales, la sintaxis contiene los siguientes elementos:

nil es un proceso que no realiza ninguna acción y se consideraprimitivo;

λ es una acción;



Sintaxis II

∑es la elección arbitraria de un proceso tomado del conjunto

de procesos indexado por I;

‖ es la composición paralela de procesos (intuitivamente, ambosprocesos pueden realizarse simultáneamente);

L es un conjunto de canales (cuyo acceso se restringirá a otrosprocesos, como se verá más adelante);

P designa a un proceso definido por medio de una expresión deltipo

P ≡def p

que puede tener carácter recursivo.



Semántica I

Las ideas anteriores se pueden expresar con más claridad por mediode reglas SOE:

Procesos resguardados

λ . p λ−→ p

Sumas

pjλ−→ q∑

i∈I piλ−→ q

j ∈ I

Composición

p0λ−→ p′0

p0 ‖ p1λ−→ p′0 ‖ p1

p1λ−→ p′1

p0 ‖ p1λ−→ p0 ‖ p′1

p0λ−→ p′0 p1

λ̄−→ p′1p0 ‖ p1

τ−→ p′0 ‖ p′1Francisco Hernández Quiroz


Semántica II

Restricción

p λ−→ q

p\L λ−→ q\Lλ 6∈ L ∪ L̄

Reetiquetamiento

p λ−→ q

p[f ]f (λ)−→ q[f ]

Identificadores

p λ−→ q

P λ−→ qdonde P ≡def p.



Ejemplos

Veamos un ejemplo muy sencillo: un buffer de capacidad 1.

Un buffer es un dispositivo de almacenamiento con capacidadfinita en el que un proceso (el productor) puede guardarinformación a la espera de que otro proceso (el consumidor) leaesta información.

La lectura destruye la información guardada.

Es importante que la información se guarde y se consuma deacuerdo con los permisos de los procesos.

El siguiente proceso de CCS se comporta de acuerdo con ladescripción anterior:

B ≡def ((α?m . β!m . nil) ‖ (β?m . γ!m . B))\{β}


Análisis lógico Lenguajes de programación

Documents

Transcript of Análisis lógico Lenguajes de programación