$ % 18-Abr-2024 \def\start{&&} \def\more{\\&&} \def\sse#1#2{{#1}\subseteq{#2}} \def\iso{\cong} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\ana#1{(\hskip -1ex[#1]\hskip -1ex )} \def\cata#1{(\hskip -1.1pt[\hskip 0.1pt #1 \hskip 0.1pt]\hskip -1.1pt)} \def\Seq#1{{#1}^{\star}} \def\fB{\fun B} \def\mcond#1#2#3{#1 \rightarrow #2\;,\;#3} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\bang{{!}} \def\Nat{\mathbb{N}} \def\N{\Nat} \def\atmost{\subseteq} \def\alt#1#2{[#1,#2]} \def\comp{\mathbin\cdot} \def\conj#1#2{\mathopen{\langle} #1, #2\mathclose{\rangle}} \def\conv#1{#1^\circ} \def\crflx#1{\Phi_{#1}} \def\dom#1{\delta {#1}} \def\from{\leftarrow} \def\fun#1{\mathsf{#1}} \def\i#1{\mathit{i}_{#1}} \def\inT{\mathsf{in}} \def\outT{\mathsf{out}} \def\implied{\Leftarrow} \def\implies{\Rightarrow} \def\just#1#2{\\& \mathopen{\{}~\mbox{#2}~\mathclose{\}}\\&&} \def\ker#1{\mathbf{ker}\ {#1}} \def\img#1{\mathbf{img}\ {#1}} \def\kons#1{\underline{#1}} \def\larrow#1#2#3{#3\ \xleftarrow{#2}\ #1} \def\ldiv{\mathbin{/}} \def\p#1{\pi_{#1}} \def\plus{\mathbin{\dagger}} \def\rarrow#1#2#3{#1\ \xrightarrow{#2}\ #3} \def\rcb#1#2#3#4{\mathopen{\langle}#1 #2 : #3 : #4\mathclose{\rangle}} \def\rdiv{\mathbin{\setminus}} \def\sep{\rule{15em}{0.3pt}} \def\shrunkby{\mathbin{\upharpoonright}} \def\syd#1#2{\frac{#1}{#2}} \def\to{\rightarrow} \def\trans#1{\overline{#1}} \def\scata#1{⦅\, #1 \,⦆} \def\sep{\rule{15em}{0.3pt}} %-------- \def\Varid#1{\mathbin{#1}} \def\ensuremath#1{#1} \def\Conid#1{\mathbin{#1}} $
Q1 - Como é que, em expressões relacionais como, por exemplo, \begin{eqnarray*} S \cap \conv P \comp R \end{eqnarray*} eu sei se o que se quer dizer é \begin{eqnarray*} S \cap (\conv P \comp R) \end{eqnarray*} ou \begin{eqnarray*} (S \cap \conv P) \comp R ~ ? \end{eqnarray*}
R: Como se disse nas aulas, para poupar parênteses associam-se prioridades aos operadores. Os unários têm prioridade máxima e, quanto aos binários, a composição ($\cdot$) tem prioridade sobre qualquer outro. Logo, $S \cap (\conv P \comp R) $ é a interpretação correcta.
As restantes prioridades são as convencionais, e.g. $(\cap) > (\cup)$, $\times > +$ etc. Nos casos em que pode haver ambiguidade, usam-se parênteses.
Q2 - Se eu tiver $\rcb\forall{a,b}{a\ X\ b}{a=b}$ posso trocar para $\rcb\forall{a,b}{a=b}{a\ X\ b}$ e depois aplicar 'one point', correcto?
R: Não (!) Isso só é válido se o quantificador for o existencial (∃). No caso do universal, a troca possível é de $\rcb\forall{a,b}{a\ X\ b}{a=b}$ para $\rcb\forall{a,b}{}{a\ X\ b \implies a=b}$ cf. a regra Trading-∀ (A.1) do formulário, para $R = true$.
Q3 - Qual é o documento recente da Casa Branca que foi mencionado na aula e que refere a relevância dos métodos formais?
R: Ver Part II: Securing the Building Blocks of Cyberspace do documento: Back to the Building Blocks - A path Toward Secure and Measurable Software (Fev.2024).
Q4 - Ainda não consigo ler bem os quadrados mágicos, pois não percebo muito bem como é que eu passo da forma sem quantificadores para a forma com quantificadores.
R: Vamos fazer a interpretação do "quadrado" \begin{eqnarray} R\ \cdot S \subseteq P \cdot Q \end{eqnarray} passo a passo: $\def\A{\rcb\exists{c}{a\ R\ c}{c\ S\ b}}\def\B{\rcb\exists{d}{a\ P\ d}{d\ Q\ b}}$ \begin{eqnarray*} \start R\ \cdot S \subseteq P \cdot Q % \just\equiv{ inclusão (5.19)} % \rcb\forall{a,b}{a(R \comp S)b}{a(P \comp Q)b} % \just\equiv{ primeira composição (5.11)} % \rcb\forall{a,b}\A{a(P \comp Q)b} % \just\equiv{ segunda composição (5.11)} % \rcb\forall{a,b}\A\B % \end{eqnarray*} Este é o caso mais geral. Versões mais simplificadas surgem quando algumas relações são funções, pois podemos usar a lei (A.6) para fazer simplificações ou, preferencialmente, a lei (5.17).
Q5 - Na aula, o Alloy que escrevi para a questão prática do blockchain foi o que se segue. Agradecia que comentasse.
sig Block {
Next : lone Block,
hash : one Word,
Phash : lone Word
}
sig Word {}
fact {
all b:Block | b.Next != b
all b:Block | b not in b.^Next
all b:Block | some b.Next => b.Next.Phash = b.hash
all b:Block | b.hash not in (Block-b).hash
one b:Block | no b.Next
one b:Block | b not in Block.Next && no b.Phash
}
run { # Next = 4} for 5 Block, 5 Word
R: As propriedades estão bem especificadas em lógica (pointwise). Algumas sugestões quanto a (re)escrevê-las em relacional pointfree:
all b:Block | b.Next != bcorresponde a $\def\Next{\mathit{Next}}\Next \cap id = \bot$ (i.é, $\Next$ é irreflexiva), em Alloy:no Next & iden;all b:Block | b not in b.^Nextcorresponde ao fecho transitivo de $\Next$ ser irreflexivo também,no ^Next & iden;all b:Block | some b.Next => b.Next.Phash = b.hashé $Phash = hash \comp \conv\Next$, em Alloy:Phash = ~Next . hash;all b:Block | b.hash not in (Block-b).hashfica garantida com a injectividade de $hash$ (em Alloy:Next.~Next in iden) para $\Next$ também injectiva.
Q6 - Não consigo identificar as funções que são pedidas no exercício 11 dos slides. Como devo abordar o problema?
R: Considerem-se as funções de $A$ para $B$. Quantas funções constantes pode haver com esse tipo? Tantas quantas os elementos de $B$. Ora, tem-se $\rarrow {Being}{where} {Bank}$ e $Bank$ tem dois elementos, $\def\Left{\mathit{Left}}\Left$ e $\def\Right{\mathit{Right}}\Right$. Logo existem as funções constantes $\kons\Right$ e $\kons\Left$, que correspondem, respetivamente, a todos os seres estarem na margem direita ou estarem todos na margem esquerda. (Repare-se que esses são os estados inicial e final do puzzle.)
Q7 - Qual é a melhor estratégia para resolver problemas como, por exemplo, a primeira alínea do exercício 20 dos slides?
R: A propriedade que se pede envolve as relações $\def\isMentorOf{\mathit{isMentorOf}}\isMentorOf$ e $\def\teaches{\mathit{teaches}}\teaches $. Ora, essas relações estão num triângulo. A estratégia é ver que orientação desse triângulo corresponde à propriedade pedida. Como queremos que "ser mentor de" implique "ser professor de", então a orientação que nos interessa é: \begin{eqnarray*} \def\Enrolls{\mathit{Enrolls}}\isMentorOf \atmost \teaches\comp\conv\Enrolls \end{eqnarray*} Já agora: Porque é que não escolhemos $\isMentorOf\comp\Enrolls \atmost \teaches $?
Q8 - No exercício 22 dos slides, primeira alínea, o que é para mostrar?
R: Uma pré ordem é uma relação reflexiva e transitiva. Logo a alínea tem duas partes: reflexividade de $\def\leqf{(\leq_f)}\leqf$, \begin{eqnarray*} id \atmost \leqf \end{eqnarray*} e a sua transitividade: \begin{eqnarray*} \leqf\comp\leqf \atmost \leqf \end{eqnarray*} Sugestões: (a) usar as leis de shunting (o mais possível) e o facto de $(\leq)$ ser, ela própria, uma pré ordem; (b) usar as regras de monotonia ("subir lado inferior" ou "descer lado superior") onde for necessário.
Q9 - No exercício 30 dos slides, o que é que se entende por a composição “preservar” uma classe relacional?
R: Há quatro classes fundamentais na taxonomia: simples, inteira, subjectiva e injectiva. A composição preservar a injectividade, por exemplo, significa mostrar que a composição de duas relações injectivas é injectiva. A mesma coisa para as outras classes.
Q10 - Relativamente à primeira ficha de exercicios não consigo perceber como desenhar o quadrado mágico que se pede na questão Q1.3.
R: Não se pede o quadrado mágico mas sim um quadrado mágico, pois há mais do que um possível. Como em \begin{eqnarray} J \subseteq \top \comp S \comp (\leq) \end{eqnarray} falta uma relação do lado inferior, basta acrescentar um $id$ e associar à esquerda, por exemplo: \begin{eqnarray} id \comp J \subseteq (\top \comp S) \comp (\leq) \end{eqnarray} Continuação: desenhar o quadrado acima identificando os quatro tipos que estão nos seus vértices.
Q11 - Eu consigo perceber o quadrado "mágico" da questão Q1.4, mas não sei (a) porque é que $\def\FS{\mathit{FS}}\FS = \kons k \comp \conv{\kons p}$ é um sistema apenas com um ficheiro; (b) que conclusões tirar do quadrado quando $\FS$ está nesse caso.
R: Quanto à alínea (a) ver exercício 4 dos slides, onde se vê que a $\kons k \comp \conv{\kons p}$ corresponde à relação singular $\{(k,p)\}$ - uma só path $p$, que conduz ao ficheiro $k$;
Alínea (b) Começando por \begin{eqnarray} \kons{Dir} \comp FS \atmost \def\type{\mathit{type}}\type \comp FS \comp parent \end{eqnarray} tem-se que $\type\ k$ é o tipo de um ficheiro, que pode ser uma directoria ($Dir$) ou não; e $p' = parent\ p$ significa que $p$ está na directoria $p'$. Substituindo $\FS$ por $\kons k \comp \conv{\kons p}$ ter-se-á: \begin{eqnarray} \kons{Dir} \comp \kons k \comp \conv{\kons p} \atmost \def\type{\mathit{type}}\type \comp \kons k \comp \conv{\kons p} \comp parent \end{eqnarray} que simplifica para \begin{eqnarray} id \atmost \conv{\kons{Dir}} \comp \kons{\type \ k} \comp \conv{\kons p} \comp \kons{parent\ p} \end{eqnarray} Porquê? (investigar os detalhes)
Introduzindo variáveis temos dois "guardanapos" fáceis de manipular. Em casa: continuar.
Q12 - No exercício 29 dos slides, não consigo mostrar que $R \cap S$ é simples desde que ou $R$ ou $S$ o sejam.
R: Por cancelamento da propriedade universal-$\cap$, i.e fazer $X := R \cap S$ em (57), tem-se $R \cap S \atmost R$ e $R \cap S \atmost S$. Ora, se $R$ for simples, então $R \cap S$ vai sê-lo também pois "mais pequeno que simples é simples" (etc)
Q13 - No exercício 31 dos slides pede-se para justificar que os isomorfismos são sempre funções bijectivas. Qual é a abordagem a seguir?
R: Um isomorfismo é estabelecido por duas funções $f$ e $g$ tal que: \begin{eqnarray*} f \comp g = id \\ g \comp f = id \end{eqnarray*} Pela primeira igualdade, $f$ deverá ser sobrejectiva e $g$ injectiva, ver slides "Meaning of $f \comp r = id$". Pela segunda igualdade, $g$ deverá ser sobrejectiva e $f$ injectiva. Logo são ambas bijectivas.
Q14 - Tenho dificuldades em escolher qual das duas alternativas da questão Q2.4 da 2ª ficha de exercícios práticos deve ser escolhida, quanto a: "se $n+1$ é o número de uma paragem de uma dada linha, então há outra paragem da mesma linha com o número $n$".
R: Repare que "se ..... então ...." vai corresponder ao "... $\atmost$ ..." na expressão relacional.
Repare ainda que "se ... então há ..." significa que vai haver uma composição no lado superior, pois composições correspondem a $\exists$ em lógica.
Logo a expressão a escolher deve ser a segunda, mas há que conformar: introduzam variáveis e confirmem que a lógica que obtém corresponde de facto ao que é pedido.
Q15 - Na resolução proposta para a Q5 do teste de 2023-05-04, não percebo o passo:
\begin{eqnarray*} \start \ensuremath{(\Varid{h},\Varid{t})\;\frac{\Varid{bag}}{\Varid{bag} \comp \mathsf{cons}}\;\Varid{x}} \just\equiv{ divisão, "guardanapo" etc} \ensuremath{(\Varid{bag} \comp \mathsf{cons})\;(\Varid{h},\Varid{t})\mathrel{=}\Varid{bag}\;\Varid{x}} \end{eqnarray*}R: Repare-se que $\frac{\Varid{bag}}{\Varid{bag} \comp \mathsf{cons}} = \conv{(bag \comp \mathsf{cons})} . bag$ pela definição de divisão de funções; o "guardanapo" aplica-se de seguida, para $R := id$ em $\conv f \comp R \comp g$, etc.
Q16 - Na resolução de um exercício aparece o passo seguinte, que eu não percebo:
\begin{eqnarray*} \start \ensuremath{\Varid{m}\mathbin{+}\mathrm{500}\leq \Varid{n}} \just\equiv{ "guardanapo" } \ensuremath{\Varid{m}\;(\conv{({+} \mathrm{500})} \comp (\leq ))\;\Varid{n}} \end{eqnarray*}R: Se se definir $f\ x = x + 500$, ficará: \begin{eqnarray*} \start f\ m \leq \Varid{n} \just\equiv{ "guardanapo" } \ensuremath{\Varid{m}\;(\conv f \comp (\leq ))\;\Varid{n}} \end{eqnarray*} Ora, $f\ x = x + 500$ é a mesma coisa que $f = (+500)$; daí aparecer $\conv f = \conv{(+500)}$.
Q17 - Dava jeito o formulário ter as taxonomias das relações e das endo-relações...
R: Na versão actual do formulário isso já acontece.
Q18 - Seguindo a sugestão dada na questão 2 deste teste de se usar a ordem de injectividade entre funções, cheguei a \begin{eqnarray*} \Varid{heldAt}\leq \conj{\Varid{takesPlace}}{\Varid{participates}} \end{eqnarray*} por analogia com um problema semelhante dos slides ("ninguém pode estar em dois lugares diferentes ao mesmo tempo"). Como represento isto sob a forma de um quadrado mágico?
R: Repare-se que ${\Varid{heldAt}\leq \conj{\Varid{takesPlace}}{\Varid{participates}}}$ expande para \begin{eqnarray*} {\ker{\conj{\Varid{takesPlace}}{\Varid{participates}}}\; \subseteq \;\ker\;\Varid{heldAt}} \end{eqnarray*} Como ${\ker{\Varid{f}}\mathrel{=}\conv{\Varid{f}} \comp \Varid{f}}$, ter-se-á o quadrado \begin{eqnarray*} \ensuremath{\conv{\conj{\Varid{takesPlace}}{\Varid{participates}}} \comp \conj{\Varid{takesPlace}}{\Varid{participates}}\; \subseteq \;\conv{\Varid{heldAt}} \comp \Varid{heldAt}} \end{eqnarray*}