1(* selftest.sml \lstset{language=ML,upquote=true}\begin{comment} % *) 2(* % 3\end{comment} % (* 4*) 5\begin{comment}==LITERATE PROGRAM FILE HEADER =======================================================\end{comment} 6 7\section{HOL Preliminaries} 8 9The HOL logic system provides a proof manager which manages the derivation of an proof. It does so using a 10structure which represents a list of assumptions, a desired conclusion, and a list of theorems from which justify the 11conclusion as drawn from the assumptions. A goal is a similar structure, without the theorems: that is, the goal consists 12of a list of assumptions and a conclusion for which a proof is desired. The derivation of a proof is a tree structure 13and can be represented using a fractional notation, where the numerator represents the goal, and the denominator represents 14a set of sub-goals which result from a mechanical application of a rule of logic. 15 16Another way of looking at a deriviation is to treat the top-most goal as the root of a tree; the sub goals sprout out 17from the root, and whenever the outermost sub-goals evaluates to true or false, it is a leaf. 18Once we have evalauted sub-goal in such a manner, the corresponding terms from the trunk can be substituted. 19 20There are a number of libraries in HOL which make this possible. One library in particular, known as `bossLib', 21provides a suite of basic automated proving tools. A number of other libraries provide type syntaxes which make it 22possible to extends HOLs native data types to include numbers, strings and lists. 23We first load these libraries and open them to make them public. 24 25Once the internal features of the bossLib structure are exposed to the HOL session, terms can now consist of expressions on strings, numbers and lists. 26As per HOL recommendations, other libraries required by the test case should be open at the front of the file befor any other commands. 27 28Following this, flags can be set to tailor the environment to the users liking. In the case of this file, to get feedback about data types and proofs, 29we enable the HOL system to display all assumptions and data types currently in use. 30 31\begin{lstlisting} % *) 32 33(* load "stringTheory"; *) 34(* val _ = load "imperativeTheory"; *) 35open HolKernel Parse boolLib bossLib numSyntax listSyntax stringTheory arithmeticTheory; 36open ptopTheory imperativeLib imperativeTheory ; 37 38val _ = set_trace "Unicode" 0; 39 40val _ = show_types:=true; 41val _ = show_assums:=true; 42 43val OK = testutils.OK 44val die = testutils.die 45val tprint = testutils.tprint; 46 47 48(* \end{lstlisting} 49 50 51\section{Theory of Imperative Programming by Example} 52 53The language of program refinement is that of logic: truth and falsehood. Truth, however, is a much loftier goal than the more practical 54problems faced by software engineers; to mistake program correctness for truth is philosophically invalid. Rather, when we speak of truth 55in a programming context, it is intended to reflect whether a final state meets a logical specification given an initial state. 56The ptopTheory defines two specifications $abort$ and $magic$, which we use when it is important to stress this interpretation of truth. 57Given any initial state and any final state, $abort$ always returns true, while $magic$ always returns false. 58Always returning true means there's no point going further -- the program has reached it's accepted limit. 59Always returning false means that you have to continue, knowing that no matter what else you do, it won't be enough to satisfy the requirements. 60 61section{Definition of Assignment } 62 63The ptopTheory defines assignment as guaranteeing that the value of a state-variable x in the next state $s'$ is equal to an expression evauated in the current state $s$. 64The following provides a test of this definition. 65 66\begin{lstlisting} % *) 67 68val _ = let val 69 xForyImplies_sx_Is_es = 70 ( 71 EVAL_RULE (SPEC ``x:'a`` (EVAL_RULE (ASSUME ``assign x e s s'``))) 72 (* [ 73 assign x e s s' 74 ] |- 75 s' x = e s : thm 76 *) 77 ) 78 79 in 80 prove ( 81 ``(\ (s :'a -> 'b) (s' :'a -> 'b).((s'(x:'a)) = ((e:('a->'b)->'b) s))) [=. (assign x e)``, 82 ( 83 (REFINEMENT_TAC) 84 (* [ 85 ] |- 86 assign x e s s' 87 ==> 88 s' x = e s 89 *) 90 THEN 91 (DISCH_TAC) 92 (* [ 93 assign x e s s' 94 ] |- 95 s' x = e s 96 *) 97 THEN 98 (ACCEPT_TAC xForyImplies_sx_Is_es) 99 ) 100 ) 101 end 102; 103 104(* \end{lstlisting} 105 106For novice users of HOL, the above code demonstrates seven commonly used tactics of the HOL proving system, namely: 107 108\begin{enumerate} 109\item{ASSUME, ASSUME_TAC} 110 111Given a theorem whose assumptions are a subset of the current goal, adds the theorems conclusion to goal's assumptions. 112 113\item{EVAL_RULE} 114 115Creates an equality between the theorems conclusion and the result of evaluating its terms and functions. 116\item{SPEC,SPECL} 117 118Allows a general theorem to be specialized to a particular instance. 119SPECL allows parallel execution of multiple SPEC tactics using a list of instances. 120\item{SUBST_TAC} 121 122Given an equality, if the left-hand side is a term in the goal, then it is replaced by the right-hand side. 123\item{DISCH_TAC} 124 125Given an implications, moves the left-hand side of the implication into the list of assumptions. 126\item{ACCEPT_TAC} 127 128Once a sub-goal has been converted into the form of an existing theorem, this tactic promotes the sub-goal to a theorem. 129\end{enumerate} 130 131\section{Sequential Composition} 132 133Sequential composition is made possible in ptopTheory by using an existential specification. 134Specifically, we assert that there exists an intermediate state, $s''$, such that initial specification $f$ provides a path from $s$ to $s''$, 135and the final specification $g$ provides a path from $s''$ to $s'$. As an example of how to use this, consider how the specification 136 137\[ s' x = 1 \and s' y = 1\] 138 139is satisfied by $y:=1;x:=y$. (here the semicolon is used to indicate sequential composition of two instructions). 140 141\begin{lstlisting} % *) 142 143fun testRefinement rhsProgLhsSpec = let val 144 lemma = 145 (UNDISCH_ALL (#1 (EQ_IMP_RULE (EVAL (mk_comb(mk_comb ((rand rhsProgLhsSpec),``s:'a->num``),``s':'a->num``)))))) 146 (* [ 147 sc (assign y (\s. 1)) (assign x (\s. s y)) s s' 148 ] |- 149 ?s''. 150 (!y'. if y = y' then s'' y' = 1 else s'' y' = s y') 151 /\ 152 (!y'. if x = y' then s' y' = s'' y else s' y' = s'' y') 153 *) 154 in 155 prove 156 ( 157 rhsProgLhsSpec, 158 ( 159 (REFINEMENT_TAC) 160 (* [ 161 ] |- 162 sc (assign y (\s. 1)) (assign x (\s. s y)) s s' ==> (s' x = 1) /\ (s' y = 1) 163 *) 164 THEN 165 (STRIP_TAC) 166 (* [ 167 sc (assign y (\s. 1)) (assign x (\s. s y)) s s' 168 ] |- 169 (s' x = 1) /\ (s' y = 1) 170 *) 171 THEN 172 (STRIP_ASSUME_TAC lemma) 173 (* [ 174 !y'. if x = y' then s' y' = s'' y else s' y' = s'' y' 175 , 176 !y'. if y = y' then s'' y' = 1 else s'' y' = s y' 177 , 178 sc (assign y (\s. 1)) (assign x (\s. s y)) s s' 179 ] |- 180 (s' x = 1) /\ (s' y = 1) 181 *) 182 THEN 183 (SUBST_TAC 184 [( 185 EVAL_RULE 186 ( 187 (SPECL [``x:'a``] (ASSUME ( #2(dest_conj (beta_conv(mk_comb((rand (concl lemma)),``s'':'a->num``))))))) 188 ) 189 )] 190 ) 191 (* [ 192 !y'. if x = y' then s' y' = s'' y else s' y' = s'' y' 193 , 194 !y'. if y = y' then s'' y' = 1 else s'' y' = s y' 195 , 196 sc (assign y (\s. 1)) (assign x (\s. s y)) s s' 197 ] |- 198 (s'' y = 1) /\ (s' y = 1) 199 *) 200 THEN 201 (SUBST_TAC 202 [( 203 EVAL_RULE 204 ( 205 (SPECL [``y:'a``] (ASSUME ( #2(dest_conj (beta_conv(mk_comb((rand (concl lemma)),``s'':'a->num``))))))) 206 ) 207 )] 208 ) 209 (* [ 210 !y'. if x = y' then s' y' = s'' y else s' y' = s'' y' 211 , 212 !y'. if y = y' then s'' y' = 1 else s'' y' = s y' 213 , 214 sc (assign y (\s. 1)) (assign x (\s. s y)) s s' 215 ] |- 216 (s'' y = 1) /\ (s'' y = 1 ) 217 *) 218 THEN 219 (CONJ_TAC THENL 220 [( 221 (* [ 222 !y'. if x = y' then s' y' = s'' y else s' y' = s'' y' 223 , 224 !y'. if y = y' then s'' y' = 1 else s'' y' = s y' 225 , 226 sc (assign y ( \s. 1)) (assign x ( \s. s y)) s s' 227 ] |- 228 (s'' y = (1 :num)) 229 *) 230 (ACCEPT_TAC 231 ( 232 EVAL_RULE 233 ( 234 (SPECL [``y:'a``] (ASSUME (#1(dest_conj (beta_conv(mk_comb((rand (concl lemma)),``s'':'a->num``))))))) 235 ) 236 ) 237 ) 238 ),( 239 (ACCEPT_TAC 240 ( 241 EVAL_RULE 242 ( 243 (SPECL [``y:'a``] (ASSUME (#1(dest_conj (beta_conv(mk_comb((rand (concl lemma)),``s'':'a->num``))))))) 244 ) 245 ) 246 ) 247 )] 248 ) 249 ) 250 ) 251 end 252 253val rhsProgRefinesLhsSpec = ``(\ (s:'a->num) (s':'a->num). (((s' (x:'a)) = 1 ) /\ ((s' (y:'a)) = 1))) [=. (sc (assign y (\ (s:'a->num).1)) (assign x (\ (s:'a->num).(s y))))``; 254 255val _ = tprint ("some implementation refines given specification: " ); 256val _ = testRefinement(rhsProgRefinesLhsSpec) handle HOL_ERR _ => die "rhsProgRefinesLhsSpec FAILED"; 257val _ = OK(); 258 259 260(* \end{lstlisting} % 261 262The example above introduces the following tactics and rules: 263 264\begin{enumerate} 265\item{UNDISCH_ALL} 266 267Given a list of assumptions, converts them into a chain of refinements. 268 269\item{EQ_IMP_RULE} 270 271Swaps the left-hand and right-hand side of an equation, as required to apply the SUBST_TAC. 272\item{STRIP_TAC,STRIP_ASSUME_TAC} 273 274Similar to DISCH_TAC, but decomposes assumptions to remove quantifiers and conjunctions so that they can be more readily used. 275\item{CONJ_TAC, EQ_TAC} 276 277If a theorem is in the form a conjunction, this breaks the goal into two sub-goals, one for the left-hand side, 278the other for the right-hand side. EQ_TAC was not used in the example, but does the same for equations. 279 280\item{rand,rator,dest_conj,beta_conv,mk_comb, concl, etc} 281 282These are a variety of routines defined in the Term structure which are useful for extracting and transforming specific 283terms into the form needed to prove a goal. 284\end{enumerate} 285 286\section{Swapping Algorithms} 287 288The final exercise is to demonstrate the use of the theory on some sample programs. 289 290A useful function on state spaces is the swap command which is defined as: 291 292(s' x = s y /\ s' y = s x) 293 294where s is free provided that s x and s y exist and are of the same type. 295Without reducing the generality of the proofs, from this point on the examples use strings (variable names) to instantiate variables $x$ and $y$ of type $'a$ 296 297We wish to show that provided $s x$, $s' x$, $s y$ and $s' y$ are the same type, the following are valid implementatons: 298 299\begin{enumerate} 300\item{in the general case } 301\item{using an algebraic method in the case where s x and s y are numeric} 302\end{enumerate} 303 304The proof benefits from a function EVAL_FOR_STATEVARS defined in imperativeLib that allows EVAL_TAC to be applied for every variable name. 305 306In the general case, we create a temporary variable and assign to it the value of one of the values to be swapped. 307The first variable is then assigned the value of the other variable, and then the other variable in turn is assigned the value of the temporary variable. 308 309\begin{lstlisting} % *) 310 311val _ = tprint ("swap is possible with introduction of temporary variable: " ); 312val GeneralSwap = let val 313 conversion = 314 PURE_ONCE_REWRITE_RULE [PREDICATIVE_SPEC_EQ_THM] 315 ( 316 SPECL 317 [ 318 ``"t"``, 319 ``(assign "x" (\ (s:string->'b). s "y"))``, 320 ``(\ (s:string->'b).s "x")`` 321 ] 322 (INST_TYPE 323 [ alpha |-> ``:string``, 324 gamma |-> ``:string->'b`` 325 ] 326 ( REFINEMENT_RULE 327 ( 328 SPECL 329 [ 330 ``f:('a->'b)->'c->bool``, 331 ``e:('a->'b)->'b``, 332 ``x:'a`` 333 ] 334 FORWARD_SUB 335 ) 336 ) 337 ) 338 ) 339 in 340 prove 341 ( 342 `` ( 343 ( 344 \ (s:string->'b) (s':string->'b) . ((s' "x") = (s "y")) /\ ((s' "y") = (s "x")) 345 ) 346 [=. 347 ( 348 sc 349 ( 350 sc (assign ("t") (\ (s:string->'b).s "x")) (assign "x" (\ (s:string->'b). s "y")) 351 ) 352 (assign "y" (\ (s:string->'b).s "t")) 353 ) 354 ) 355 `` 356 , 357 (SUBST_TAC [conversion]) 358 (* [ 359 ] |- 360 (\s s'. (s' "x" = s "y") /\ (s' "y" = s "x")) [=. sc (subs (assign "x" (\s. s "y")) "t" (\s. s "x")) (assign "y" (\s. s "t")) 361 *) 362 THEN 363 (REP_EVAL_TAC) 364 (* [ 365 ] |- 366 !s s'. 367 (?s''. 368 (!y.if "x" = y then s'' y = s "y" else s' y = if "t" = y then s "x" else s y) 369 /\ 370 (!y. if "y" = y then s' y = s'' "t" else s' y = s'' y) 371 ) 372 ==> 373 (s' "x" = s "y") /\ (s' "y" = s "x") 374 *) 375 376 THEN 377 (REPEAT STRIP_TAC) 378 THEN 379 (EVAL_FOR_STATEVARS [``"t"``,``"x"``,``"y"``]) 380 THEN 381 REP_EVAL_TAC 382 ) 383 end 384handle HOL_ERR _ => die "general swap FAILED"; 385val _ = OK(); 386 387(* \end{lstlisting} 388 389In the special case where both variables are numbers, an algebraic method can be used to swap the values without the use of a temporary variable. 390 391\begin{lstlisting} % *) 392 393(* 394 need this for LESS_EQ_REFL, LESS_EQ_ADD_SUB, SUB_EQ_0, and ADD_0 395 396*) 397 398val _ = tprint ("swap is possible for num type without need for temporary variable: " ); 399val NumericSwap = let val 400 conversion = 401 PURE_ONCE_REWRITE_RULE [PREDICATIVE_SPEC_EQ_THM] 402 ( 403 SPECL 404 [ 405 ``"x"``, 406 ``(assign "y" (\ (s:string->num). ((s "x") - (s "y"))))``, 407 ``(\ (s:string->num).((s "x") + (s "y")))`` 408 ] 409 (INST_TYPE 410 [ 411 alpha |-> ``:string``, 412 beta |-> ``:num``, 413 gamma |-> ``:string->num`` 414 ] 415 ( REFINEMENT_RULE 416 ( 417 SPECL 418 [ 419 ``f:('a->'b)->'c->bool``, 420 ``e:('a->'b)->'b``, 421 ``x:'a`` 422 ] FORWARD_SUB 423 ) 424 ) 425 ) 426 ) 427 and 428 lemma = prove (``!(a:num) (b:num). (a + b -(a + b -b)) = (b + a - a)``,(PROVE_TAC [LESS_EQ_REFL, LESS_EQ_ADD_SUB, SUB_EQ_0,ADD_0,ADD_SYM])) 429 in 430 prove 431 ( 432 `` 433 ( 434 \ (s:string->num) (s':string->num). ((s' "x") = (s "y")) /\ ((s' "y") = (s "x")) 435 ) 436 [=. 437 ( 438 sc 439 ( 440 ( sc 441 (assign "x" (\ (s:string->num).((s "x") + (s "y")))) 442 (assign "y" (\ (s:string->num). ((s "x") - (s "y")))) 443 ) 444 ) 445 ( 446 assign "x" (\ (s:string->num).((s "x") - (s "y"))) 447 ) 448 ) 449 `` 450 , 451 (SUBST_TAC [conversion]) 452 (* [ 453 ] |- 454 (\(s :string -> num) (s' :string -> num). (s' "x" = s "y") /\ (s' "y" = s "x")) 455 [=. 456 sc 457 (subs (assign "y" (\(s :string -> num). s "x" - s "y")) "x" 458 (\(s :string -> num). s "x" + s "y")) 459 (assign "x" (\(s :string -> num). s "x" - s "y")) 460 *) 461 THEN 462 (REP_EVAL_TAC) 463 THEN 464 (REPEAT STRIP_TAC) 465 THEN 466 (EVAL_FOR_STATEVARS [``"x"``,``"y"``]) 467 THEN 468 (PROVE_TAC [LESS_EQ_REFL, LESS_EQ_ADD_SUB, SUB_EQ_0,ADD_0,lemma]) 469 ) 470 end 471handle HOL_ERR _ => die "numeric swap FAILED"; 472val _ = OK(); 473 474(* \end{lstlisting} 475 476 477This concludes the demonstration. 478 479\begin{comment}===LITERATE PROGRAM FILE TRAILER =======================================================\end{comment} 480 \begin{lstlisting} 481(* 482 Last updated April 3, 2017 483*) 484\end{lstlisting} % 485% *) 486