diff options
author | Nguyễn Gia Phong <cnx@loang.net> | 2023-11-24 18:08:17 +0900 |
---|---|---|
committer | Nguyễn Gia Phong <cnx@loang.net> | 2023-11-24 18:08:17 +0900 |
commit | 679ca723e849b731a9d94a276763bb59756aa3a2 (patch) | |
tree | 95d45dc5657288a881b32c92051d795ea315cc9e /bg.tex | |
parent | cf32a3f1cac556281aafa02355fbec106f00edd5 (diff) | |
download | thesis-679ca723e849b731a9d94a276763bb59756aa3a2.tar.gz |
Proof read approach
Diffstat (limited to 'bg.tex')
-rw-r--r-- | bg.tex | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/bg.tex b/bg.tex index ba2f131..4c12048 100644 --- a/bg.tex +++ b/bg.tex @@ -20,31 +20,31 @@ which is omitted from the algorithm for brevity. \Require Program ($P$) \Ensure Set of test cases ($T$) \State $T \gets \varnothing$ - \State $S \gets \textsc{InitialState}(P)$ \Comment{set of states} + \State $S \gets \Call{InitialState}{P}$ \Comment{set of states} \While{$S \neq \varnothing$} - \State $s \gets \textsc{Select}(S)$ + \State $s \gets \Call{Select}{S}$ \State $S \gets S \setminus \{s\}$ - \State $i, e, \varPhi \gets s$ + \State $(i, e, \varPhi) \gets s$ \Comment{instruction, environment, and path constraints} - \State $i', e' \gets \textsc{Execute}(i, e)$ - \If{$\textsc{IsHalt}(i)$} - \State $t \gets \textsc{GenerateTest}(\varPhi)$ + \State $(i', e') \gets \Call{Execute}{i, e}$ + \If{$\Call{IsHalt}{i}$} + \State $t \gets \Call{GenerateTest}{\varPhi}$ \If{$t \ne \bot$} $T \gets T \cup \{t\}$ \EndIf - \ElsIf{$\textsc{IsBranch}(i)$} - \State $\varphi, i_c', i_a' \gets i'$ + \ElsIf{$\Call{IsBranch}{i}$} + \State $(\varphi, i_c', i_a') \gets i'$ \Comment{condition, consequent, and alternative} - \If{$\textsc{sat}(\varPhi \land \varphi)$} - \State $s_c' \gets i_c', e', \varPhi \land \varphi$ + \If{$\Call{sat}{\varPhi \land \varphi}$} + \State $s_c' \gets (i_c', e', \varPhi \land \varphi)$ \State $S \gets S \cup \{s_c'\}$ \EndIf - \If{$\textsc{sat}(\varPhi \land \lnot\varphi)$} + \If{$\Call{sat}{\varPhi \land \lnot\varphi}$} \State $s_a' \gets i_a', e', \varPhi \land \lnot\varphi$ \State $S \gets S \cup \{s_a'\}$ \EndIf \Else - \State $s' \gets i', e', \varPhi$ + \State $s' \gets (i', e', \varPhi)$ \State $S \gets S \cup \{s'\}$ \EndIf \EndWhile |