csi2324f02

$ % 01-Mar-2024 \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\implied{\Leftarrow} \def\implies{\Rightarrow} \def\just#1#2{\\&#1& \mathopen{\{}~\mbox{#2}~\mathclose{\}}\\&&} \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}} $

Q2.1 - A figura representa um blockchain elementar com cinco blocos. Cada bloco tem o seu $hash$ e o hash do bloco anterior ($\def\Phash{\mathit{Phash}}\Phash$), caso exista.

Identifique as relações que são:

simples
injectivas
reflexivas
irreflexivas
inteiras

Q2.2 - Represente sob a forma de um diagrama com os tipos $Block$ e $\def\Word{\mathit{Word}}\Word$ o modelo relacional que o diagrama da questão anterior sugere e acrescente-lhe os invariantes seguintes:

A função $hash$ tem de ser injectiva
Um bloco não pode ter mais do que um bloco sucessor e um bloco anterior
$\Phash$ deve dar exactamente o $hash$ do bloco anterior, caso exista.

$\Box$

Q2.3 - $\tiny\sf\fbox{Alloy for fun}$ Complete o modelo Alloy abaixo e verifique-o na plataforma Alloy for fun:

sig Block { 
  Next  : lone Block, 
  hash  : one Word, 
  Phash : lone Word 
}

sig Word {}

fact {
   .....
}

run { # Next = 4} for 5 Block, 5 Word

$\Box$

Q2.4 - Pretende-se especificar o metro de Tóquio onde (cf. figura) há várias linhas ($L$) representadas com cores diferentes, cujas paragens ($P$) estão numeradas sequencialmente e onde as estações ($E$) podem incluir paragens de linhas diferentes $-\!-$ e.g. a estação $\mathsf{Otemachi}$ tem as paragens $\fbox{$\frac C {11}$}$, $\fbox{$\frac M {18}$}$, etc $-\!-$ permitindo aos viajantes mudar de linha.

Sabendo-se que cada paragem está sempre associada a uma e uma só estação, definiu-se o modelo simplificado

que a cada paragem associa a respectiva linha, número e estação. Por exemplo, sendo $p$ a paragem $\fbox{$\frac M {18}$}$ da figura, ter-se-á

$\begin{array}{l}st\ p = Otemachi\\\mathit{ln}\ p = M\\nr\ p = 18\end{array}$.

Claramente, o sistema de numeração das paragens das linhas necessita do seguinte invariante:

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$.

Qual das seguintes formulações desse invariante escolheria,

\begin{eqnarray} && \frac{nr}{succ \cdot nr} \subseteq \frac{ln}{ln} \label{eq:181128a} \\&& \nonumber\\&& \frac{nr}{succ} \subseteq nr \cdot \frac{ln}{ln} \end{eqnarray}

onde $succ\ n = n+1$ é a função sucessor em $\Nat$?

Converta cada "quadrado mágico" na expressão lógica equivalente e decida, justificando.

$\Box$

CSI/2324 - Folha de exercícios nr. 2¶

➡️ Aula de 13-Mar-2024¶