summary refs log tree commit diff homepage
path: root/bg.tex
diff options
context:
space:
mode:
authorNguyễn Gia Phong <cnx@loang.net>2023-11-24 18:08:17 +0900
committerNguyễn Gia Phong <cnx@loang.net>2023-11-24 18:08:17 +0900
commit679ca723e849b731a9d94a276763bb59756aa3a2 (patch)
tree95d45dc5657288a881b32c92051d795ea315cc9e /bg.tex
parentcf32a3f1cac556281aafa02355fbec106f00edd5 (diff)
downloadthesis-679ca723e849b731a9d94a276763bb59756aa3a2.tar.gz
Proof read approach
Diffstat (limited to 'bg.tex')
-rw-r--r--bg.tex24
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