Lista de Exercícios 4 - Teoria da computação

Prévia do material em texto

1	
Universidade	Federal	de	Viçosa	Centro	de	Ciências	Exatas	e	Tecnológicas	Departamento	de	Informática	
INF130	–	Teoria	da	Computação	11/11/2015		 4ª	Lista	de	Exercícios		Verifique,	pela	lógica	de	Hoare,	a	correção	(parcial)	das	seguintes	funções.	Quando	não	houver	a	pré-condição	inicial,	tente	determinar	a	mais	fraca	possível	para	que	se	obtenha	a	pós-condição	final	dada.	Escreva,	nas	lacunas	dos	comentários,	as	asserções	válidas,	usando	(a	linguagem	da)	lógica	de	primeira	ordem.		 1. Cálculo	da	divisão	inteira,	obtendo	o	quociente	e	o	resto,	onde	o	invariante	para	o	laço	principal	é:	𝐼 ≡ (𝑞 ∗ 𝑦 + 𝑟 = 𝑥) ∧ (𝑟 ≥ 0).		
void quoc(int x, int y, int &q, int &r) 
{ 
 /* __________________________________________ */ 
 r = x; 
 /* __________________________________________ */ 
 q = 0; 
 /* __________________________________________ */ 
 while (y ≤ r) 
 { 
 /* _______________________________________ */ 
 q = q + 1; 
 /* _______________________________________ */ 
 r = r – y; 
 /* _______________________________________ */ 
 } 
 /* 𝑞 ∗ 𝑦 + 𝑟 = 𝑥 ∧ (0 ≤ 𝑟 < 𝑦) */ 
} 	 2. Cálculo	do	máximo	divisor	comum,	onde	o	invariante	do	laço	principal	é	dado	por	𝐼 ≡ mdc 𝑎, 𝑏 = mdc(𝑥,𝑦).		
int mdc(int x, int y) 
{ 
 /* (𝑥 > 0) ∧ (𝑦 > 0) */ 
 a = x; 
 /* ___________________________________________ */ 
 b = y; 
 /* ___________________________________________ */ 
 while (a != b) 
 { 
 /* ________________________________________ */ 
 if (a > b) 
 /* _____________________________________ */ 
 a = a – b; 
	 2	
 /* ______________________________________ */ 
 else 
 /* ______________________________________ */ 
 b = b – a; 
 } 
 /* ____________________________________________ */ 
 return a; 
 /* 𝑎 = 𝑏 = mdc(𝑥,𝑦) */ 
} 
 Sugestão:	Talvez	você	precisará	das	seguintes	relações	conhecidas	do	mdc:		 mdc 𝑢, 𝑣 = mdc 𝑢 − 𝑣, 𝑣 , se 𝑢 > 𝑣	mdc 𝑢, 𝑣 = mdc(𝑣,𝑢)	mdc 𝑢,𝑢 = 𝑢		 3. Produto	eficiente	de	números	inteiros,	onde	o	invariante	do	laço	principal	é	dado	por	𝐼 ≡ (𝑧 + 𝑢 ∗ 𝑣 = 𝑥 ∗ 𝑦) ∧ (𝑢 ≥ 0).	O	predicado	odd(𝑢)	é	satisfeito	se	𝑢	for	um	número	ímpar.		
int prod(int x, int y) 
{ 
 /* _____________________________________________ */ 
 int u, v, z; 
 /* _____________________________________________ */ 
 u = x; 
 /* _____________________________________________ */ 
 v = y; 
 /* _____________________________________________ */ 
 z = 0; 
 /* _____________________________________________ */ 
 while (u != 0) 
 { 
 /* __________________________________________ */ 
 if (odd(u)) 
 /* _______________________________________ */ 
 z = z + v; 
 /* __________________________________________ */ 
 u = u / 2; 
 /* __________________________________________ */ 
 v = 2 * v; 
 /* __________________________________________ */ 
 } 
 /* _____________________________________________ */ 
 return z; 
 /* 𝑧 = 𝑥 ∗ 𝑦 */