Lines Matching refs:value
99 ``wp (While g (body:value command)) Inv = (\s. if g s then wp body (wp (While g body) Inv) s else Inv s)``,
1505 ``!(i :string) (n :string) (body :value command).
1508 (\(s :value state).
1510 (\(s :value state). (0 :int) <= int_of_value (s i)) s
1518 (\(s :value state).
1520 (\(s :value state). (0 :int) <= int_of_value (s i)) s
1529 (\(s :value state).
1531 (\(s :value state).
1533 (\(s :value state). (0 :int) <= int_of_value (s i))
1535 ((\(s :value state).
1545 (\(s :value state).
1547 (\(s :value state).
1556 (\(s :value state).
1558 (\(s :value state). (0 :int) <= int_of_value (s i)) s
1567 (\(s :value state).
1571 (\(s :value state).
1573 (One :value state expect))``,
1575 ++ Q.ABBREV_TAC `Inv = (\(s :value state). (0 :int) <= int_of_value (s (i :string)))`
1576 ++ Q.ABBREV_TAC `g = (\(s :value state).
1579 ++ Q.ABBREV_TAC `Var = (\(s :value state).
1582 ++ Q.ABBREV_TAC `loopbody = Seq (body :value command)
1584 (\(s :value state). Int (int_of_value (s i) + (1 :int))))`
1587 (\(s :value state).
1588 (if (g :value state -> bool) s /\ (Inv :value state -> bool) s then
1594 (wp (loopbody :value command)
1595 (\(s :value state).
1602 (wp (body :value command)
1603 (\(s :value state).
1605 (\(s :value state). (0 :int) <= int_of_value (s (i :string)))
1614 (\(s :value state).
1626 (\(s :value state).
1636 (\(s :value state).
1637 (if (\(s :value state). (0 :int) <= int_of_value (s i)) s then
1649 (\(s :value state).
1651 (g :value state -> bool) s /\ (Inv :value state -> bool) s /\
1652 ((Var :value state -> int) s = N)
1659 (wp (loopbody :value command)
1660 (\(s :value state).
1668 ++ `(\(s :value state).
1678 (\(s :value state).
1680 (\(s :value state). int_of_value (s n) - int_of_value (s i)) s <=
1689 ++ `int_of_value ((s :value state) (n :string)) -
1692 by (`int_of_value ((s :value state) (n :string)) =
1702 (\(s :value state).
1704 (g :value state -> bool) s /\ (Inv :value state -> bool) s /\
1705 ((Var :value state -> int) s = N)
1712 (wp (loopbody :value command)
1713 (\(s :value state).
1716 ++ `wp (loopbody :value command)
1717 (\(s :value state).
1719 (Inv :value state -> bool) s /\
1720 (Var :value state -> int) s < (N :int)
1729 (\(s :value state). (if Inv s then (1 :posreal) else (0 :posreal)))
1730 (\(s :value state).
1732 by (`(\(s :value state).
1734 (Inv :value state -> bool) s /\
1735 (Var :value state -> int) s < (N :int)
1742 Conj (\(s :value state). (if Inv s then (1 :posreal) else (0 :posreal)))
1743 (\(s :value state).
1752 (\(s :value state).
1754 (g :value state -> bool) s /\ (Inv :value state -> bool) s /\
1755 ((Var :value state -> int) s = (N :int))
1763 (\(s :value state).
1765 (\(s :value state).
1777 (\(s :value state).
1779 (g :value state -> bool) s /\ (Inv :value state -> bool) s
1786 (\(s :value state).
1788 g s /\ Inv s /\ ((Var :value state -> int) s = (N :int))
1795 (wp (loopbody :value command)
1797 (\(s :value state).
1799 (\(s :value state).
1805 (wp (loopbody :value command)
1806 (\(s :value state).
1807 (if (Inv :value state -> bool) s then
1814 (\(s :value state).
1815 (if (Var :value state -> int) s < (N :int) then
1823 (\(s :value state).
1825 (\(s :value state).
1830 (\(s :value state).
1832 (g :value state -> bool) s /\ (Inv :value state -> bool) s
1839 (\(s :value state).
1841 g s /\ Inv s /\ ((Var :value state -> int) s = (N :int))
1849 (wp (loopbody :value command)
1850 (\(s :value state).
1853 (\(s :value state).
1864 (\(s :value state).
1866 (Inv :value state -> bool) s /\
1867 (Var :value state -> int) s < (1 :int) + (& N :int)
1874 (While (\(s :value state). (g :value state -> bool) s)
1875 (loopbody :value command)) (One :value state expect))`
1880 (\(s :value state).
1882 (Inv :value state -> bool) s /\
1883 (Var :value state -> int) s < (1 :int)
1890 (\(s :value state).
1891 (if ~(g :value state -> bool) s then
1903 ++ `(0 :int) + int_of_value ((s :value state) (i :string)) <
1907 int_of_value ((s :value state) (n :string)) -
1912 (\(s :value state).
1913 (if ~(g :value state -> bool) s then
1919 (wp (While (\(s :value state). g s) (loopbody :value command))
1920 (One :value state expect))`
1925 ((expect :value state expect -> bool),
1926 (Leq :value state expect -> value state expect -> bool))
1927 (\(e :value state expect) (s :value state).
1928 (if (g :value state -> bool) s then
1929 wp (loopbody :value command) e s
1937 ((expect :value state expect -> bool),
1938 (Leq :value state expect -> value state expect -> bool))
1939 (\(e :value state expect) (s :value state).
1940 (if (g :value state -> bool) s then
1941 wp (loopbody :value command) e s
1945 (\(e :value state expect) (s :value state).
1950 (\(s :value state).
1951 (if (g :value state -> bool) s then
1952 wp (loopbody :value command)
1954 (\(e :value state expect) (s :value state).
1957 One s)) (s :value state)`
1962 (\(s :value state).
1964 (Inv :value state -> bool) s /\
1965 (Var :value state -> int) s < (1 :int) + (& (SUC (N :num)) :int)
1972 (\(s :value state).
1973 (\(s :value state).
1974 (if (g :value state -> bool) s then
1980 (\(s :value state).
1986 (\(s :value state).
1987 (\(s :value state).
1989 (\(s :value state).
2000 (\(s :value state).
2001 (\(s :value state).
2002 (if (g :value state -> bool) s then
2008 (\(s :value state).
2010 (Inv :value state -> bool) s /\
2011 (Var :value state -> int) s <
2018 (\(s :value state).
2019 (\(s :value state).
2021 (\(s :value state).
2027 (wp (While (\(s :value state). g s) (loopbody :value command))
2028 (One :value state expect))`
2032 (\(s :value state).
2033 (if ~(g :value state -> bool) s then
2039 (wp (While (\(s :value state). g s) (loopbody :value command))
2040 (One :value state expect))`
2045 ((expect :value state expect -> bool),
2046 (Leq :value state expect -> value state expect -> bool))
2047 (\(e :value state expect) (s :value state).
2048 (if (g :value state -> bool) s then
2049 wp (loopbody :value command) e s
2057 ((expect :value state expect -> bool),
2058 (Leq :value state expect -> value state expect -> bool))
2059 (\(e :value state expect) (s :value state).
2060 (if (g :value state -> bool) s then
2061 wp (loopbody :value command) e s
2065 (\(e :value state expect) (s :value state).
2070 (\(s :value state).
2071 (if (g :value state -> bool) s then
2072 wp (loopbody :value command)
2074 (\(e :value state expect) (s :value state).
2077 One s)) (s :value state)`
2082 (\(s :value state).
2083 (\(s :value state).
2084 (if (g :value state -> bool) s then
2090 (\(s :value state).
2092 (Inv :value state -> bool) s /\
2093 (Var :value state -> int) s <
2100 (\(s :value state).
2101 (\(s :value state).
2103 (\(s :value state).
2110 (\(s :value state).
2111 (\(s :value state).
2113 (\(s :value state).
2119 (wp (While (\(s :value state). g s) (loopbody :value command))
2120 (One :value state expect)))`
2127 (While (\(s :value state). (g :value state -> bool) s)
2128 (loopbody :value command)) (One :value state expect)
2129 (s :value state)`
2136 (\(s :value state).
2137 (\(s :value state).
2138 (if (g :value state -> bool) s then
2144 (\(s :value state).
2146 (Inv :value state -> bool) s /\
2147 (Var :value state -> int) s <
2154 (wp (While (\(s :value state). g s) (loopbody :value command))
2155 (One :value state expect)))
2156 (wp (While (\(s :value state). g s) loopbody)
2157 (One :value state expect))`
2162 (\(s :value state).
2163 (\(s :value state).
2164 (if (g :value state -> bool) s then
2170 (\(s :value state).
2172 (Inv :value state -> bool) s /\
2173 (Var :value state -> int) s <
2180 (wp (While (\(s :value state). g s) (loopbody :value command))
2181 (One :value state expect)))
2184 (\(s :value state).
2190 (\(s :value state).
2196 (wp (While (\(s :value state). g s) loopbody)
2197 (One :value state expect)))`
2199 ++ `(Var :value state -> int) (s :value state) <
2203 ++ `(Var :value state -> int) (s :value state) <=
2219 (\(s :value state).
2221 (g :value state -> bool) s /\
2222 (Inv :value state -> bool) s /\
2223 (Var :value state -> int) s < (1 :int) + (& (N :num) :int)
2229 (\(s :value state).
2235 (wp (While (\(s :value state). g s) (loopbody :value command))
2236 (One :value state expect)))
2237 (wp (While (\(s :value state). g s) loopbody)
2238 (One :value state expect))`
2244 (\(s :value state).
2246 (g :value state -> bool) s /\
2247 (Inv :value state -> bool) s /\
2248 (Var :value state -> int) s < (1 :int) + (& (N :num) :int)
2254 (\(s :value state).
2260 (wp (While (\(s :value state). g s) (loopbody :value command))
2261 (One :value state expect)))
2264 (\(s :value state).
2266 wp (While (\(s :value state). g s) loopbody)
2267 (One :value state expect) s)
2268 (\(s :value state).
2274 (wp (While (\(s :value state). g s) loopbody)
2275 (One :value state expect)))`
2282 (While (\(s :value state). (g :value state -> bool) s)
2283 (loopbody :value command)) (One :value state expect)
2284 (s :value state))
2285 (wp (While (\(s :value state). g s) loopbody)
2286 (One :value state expect) s) =
2287 wp (While (\(s :value state). g s) loopbody) (One :value state expect) s`
2292 (While (\(s :value state). (g :value state -> bool) s)
2293 (loopbody :value command)) (One :value state expect)
2294 (s :value state)) (posreal_pow (1 :posreal) (N :num)))
2295 (wp (While (\(s :value state). g s) loopbody)
2296 (One :value state expect) s) =
2298 (wp (While (\(s :value state). g s) loopbody)
2299 (One :value state expect) s)`
2305 (\(s :value state).
2308 (While (\(s :value state). (g :value state -> bool) s)
2309 (loopbody :value command)) (One :value state expect) s)
2310 (\(s :value state).
2312 g s /\ (Inv :value state -> bool) s /\
2313 ((Var :value state -> int) s =
2320 (wp (While (\(s :value state). g s) loopbody)
2321 (One :value state expect)))
2322 (wp (While (\(s :value state). g s) loopbody)
2323 (One :value state expect))`
2329 (\(s :value state).
2332 (While (\(s :value state). (g :value state -> bool) s)
2333 (loopbody :value command)) (One :value state expect) s)
2334 (\(s :value state).
2336 g s /\ (Inv :value state -> bool) s /\
2337 ((Var :value state -> int) s =
2344 (wp (While (\(s :value state). g s) loopbody)
2345 (One :value state expect)))
2347 (\(s :value state).
2350 (\(s :value state).
2357 (wp (While (\(s :value state). g s) loopbody)
2358 (One :value state expect)))`
2363 (While (\(s :value state). (g :value state -> bool) s)
2364 (loopbody :value command)) (One :value state expect)
2365 (s :value state))
2367 g s /\ (Inv :value state -> bool) s /\
2368 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int))
2374 (wp (While (\(s :value state). g s) loopbody)
2375 (One :value state expect) s) =
2382 (wp (While (\(s :value state). g s) loopbody)
2383 (One :value state expect) s)`
2387 (While (\(s :value state). (g :value state -> bool) s)
2388 (loopbody :value command)) (One :value state expect)
2389 (s :value state))
2391 g s /\ (Inv :value state -> bool) s /\
2392 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int))
2398 (wp (While (\(s :value state). g s) loopbody)
2399 (One :value state expect) s) =
2407 (wp (While (\(s :value state). g s) loopbody)
2408 (One :value state expect) s)
2409 (wp (While (\(s :value state). g s) loopbody)
2410 (One :value state expect) s))`
2416 (g :value state -> bool) (s :value state) /\
2417 (Inv :value state -> bool) s /\
2418 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int))
2436 (g :value state -> bool) (s :value state) /\
2437 (Inv :value state -> bool) s /\
2438 ((Var :value state -> int) s = (1 :int) + (& N :int))
2446 wp (loopbody :value command)
2447 (\(s :value state).
2455 (g :value state -> bool) (s :value state) /\
2456 (Inv :value state -> bool) s /\
2457 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int))
2464 wp (loopbody :value command)
2465 (\(s :value state).
2480 (\(s :value state).
2482 wp (loopbody :value command)
2483 (\(s :value state).
2485 (Inv :value state -> bool) s /\
2486 (Var :value state -> int) s < (1 :int) + (& N :int)
2494 (While (\(s :value state). (g :value state -> bool) s) loopbody)
2495 (One :value state expect)))
2496 (wp (While (\(s :value state). g s) loopbody)
2497 (One :value state expect))`
2500 ++ `(\(s :value state).
2502 wp (loopbody :value command)
2503 (\(s :value state).
2505 (Inv :value state -> bool) s /\
2506 (Var :value state -> int) s < (1 :int) + (& N :int)
2514 (\(s :value state).
2521 ++ `(\(s :value state).
2523 (Inv :value state -> bool) s /\
2524 (Var :value state -> int) s < (1 :int) + (& (N :num) :int)
2530 (\(s :value state).
2542 wp (loopbody :value command)
2543 (\(s :value state).
2545 (Inv :value state -> bool) s /\
2546 (Var :value state -> int) s < (1 :int) + (& N :int)
2552 posreal))) (s :value state) =
2554 (\(s :value state).
2556 (\(s :value state).
2569 (wp (loopbody :value command)
2570 (\(s :value state).
2572 (Inv :value state -> bool) s /\
2573 (Var :value state -> int) s < (1 :int) + (& (N :num) :int)
2580 (While (\(s :value state). (g :value state -> bool) s) loopbody)
2581 (One :value state expect)))
2584 (wp (While (\(s :value state). g s) loopbody)
2585 (One :value state expect)))
2586 (wp (While (\(s :value state). g s) loopbody)
2587 (One :value state expect)))`
2589 (wp (loopbody :value command)
2590 (\(s :value state).
2592 (Inv :value state -> bool) s /\
2593 (Var :value state -> int) s < (1 :int) + (& (N :num) :int)
2601 (While (\(s :value state). (g :value state -> bool) s) loopbody)
2602 (One :value state expect)))`
2610 (wp (loopbody :value command)
2612 (While (\(s :value state). (g :value state -> bool) s)
2613 loopbody) (One :value state expect)))
2614 (wp (While (\(s :value state). g s) loopbody)
2615 (One :value state expect)))
2616 (wp (While (\(s :value state). g s) loopbody)
2617 (One :value state expect))`
2621 (wp (loopbody :value command)
2623 (While (\(s :value state). (g :value state -> bool) s) loopbody)
2624 (One :value state expect)))
2625 (wp (While (\(s :value state). g s) loopbody)
2626 (One :value state expect))`
2628 ((expect :value state expect -> bool),
2629 (Leq :value state expect -> value state expect -> bool))
2630 (\(e :value state expect) (s :value state).
2631 (if (g :value state -> bool) s then
2632 wp (loopbody :value command) e s
2640 ((expect :value state expect -> bool),
2641 (Leq :value state expect -> value state expect -> bool))
2642 (\(e :value state expect) (s :value state).
2643 (if (g :value state -> bool) s then
2644 wp (loopbody :value command) e s
2648 (\(e :value state expect) (s :value state).
2653 ++ Suff `wp (loopbody :value command)
2655 (\(e :value state expect) (s :value state).
2656 (if (g :value state -> bool) s then
2659 One s))) (s :value state) <=
2660 (\(s :value state).
2664 (\(e :value state expect) (s :value state).
2671 (\(e :value state expect) (s :value state).
2672 (if (g :value state -> bool) s then
2673 wp (loopbody :value command) e s
2677 wp (While (\(s :value state). g s) loopbody) (One :value state expect)`
2681 ++ `wp (loopbody :value command)
2682 (wp (While (\(s :value state). (g :value state -> bool) s) loopbody)
2683 (One :value state expect)) (s :value state) =
2684 wp (Seq loopbody (While (\(s :value state). g s) loopbody))
2685 (One :value state expect) s`
2693 (\(s :value state).
2695 (Inv :value state -> bool) s /\
2696 (Var :value state -> int) s < (1 :int) + (& N :int)
2704 (While (\(s :value state). (g :value state -> bool) s)
2705 (loopbody :value command)) (One :value state expect))`
2707 ++ `(\(s :value state).
2708 (if (Inv :value state -> bool) s then
2715 (\(s :value state).
2716 (if (g :value state -> bool) s /\ Inv s then
2722 (\(s :value state).
2731 (\(s :value state).
2733 (g :value state -> bool) s /\ (Inv :value state -> bool) s
2740 (\(s :value state).
2743 (\(s :value state).
2745 (wp (While (\(s :value state). g s) (loopbody :value command))
2746 (One :value state expect)))`
2748 (\(s :value state).
2749 (if ~(g :value state -> bool) s then
2755 (wp (While (\(s :value state). g s) (loopbody :value command))
2756 (One :value state expect))`
2761 ((expect :value state expect -> bool),
2762 (Leq :value state expect -> value state expect -> bool))
2763 (\(e :value state expect) (s :value state).
2764 (if (g :value state -> bool) s then
2765 wp (loopbody :value command) e s
2773 ((expect :value state expect -> bool),
2774 (Leq :value state expect -> value state expect -> bool))
2775 (\(e :value state expect) (s :value state).
2776 (if (g :value state -> bool) s then
2777 wp (loopbody :value command) e s
2781 (\(e :value state expect) (s :value state).
2786 (\(s :value state).
2787 (if (g :value state -> bool) s then
2788 wp (loopbody :value command)
2790 (\(e :value state expect) (s :value state).
2793 One s)) (s :value state)`
2803 (\(s :value state).
2805 (g :value state -> bool) s /\ (Inv :value state -> bool) s
2812 (wp (While (\(s :value state). g s) (loopbody :value command))
2813 (One :value state expect)))
2814 (wp (While (\(s :value state). g s) loopbody)
2815 (One :value state expect))`
2819 (\(s :value state).
2820 (if (g :value state -> bool) s /\ (Inv :value state -> bool) s then
2826 (wp (While (\(s :value state). g s) (loopbody :value command))
2827 (One :value state expect))`
2839 >> (`?(n'' :num). int_of_value ((s :value state) (n :string)) = (& n'' :int)` by METIS_TAC [NUM_POSINT_EXISTS, INT_LT_IMP_LE, INT_LE_TRANS]
2841 int_of_value ((s :value state) (i :string)) <
2908 (0 :int) <= int_of_value ((s :value state) (i :string)) /\
2918 (While (\(s :value state). int_of_value (s i) < int_of_value (s n))
2919 (Seq (body :value command)
2921 (\(s :value state). Int (int_of_value (s i) + (1 :int))))))
2922 (One :value state expect) s`
2931 ``!(i :string) (n :string) (body :value command list).
2934 (\(s :value state).
2936 (\(s :value state). (0 :int) <= int_of_value (s i)) s
2944 (\(s :value state).
2946 (\(s :value state). (0 :int) <= int_of_value (s i)) s
2955 (\(s :value state).
2957 (\(s :value state).
2959 (\(s :value state). (0 :int) <= int_of_value (s i))
2961 ((\(s :value state).
2971 (\(s :value state).
2973 (\(s :value state).
2981 (wp (For_0_to_n i n body) (One :value state expect) =
2982 (One :value state expect))``,
2987 (Seq (Assign (i :string) (\(s :value state). Int (0 :int)))
2989 (\(s :value state).
2991 (Seq (Program (body :value command list))
2993 (\(s :value state).
2995 (\(s :value state expect).
2996 wp (Assign i (\(s :value state). Int (0 :int)))
2999 (\(s :value state). int_of_value (s i) < int_of_value (s n))
3002 (\(s :value state).
3008 ++ `wp (Assign (i :string) (\(s :value state). Int (0 :int))) =
3009 (\(r :value state expect) (s :value state).
3010 r (assign i (\(s :value state). Int (0 :int)) s))`
3017 (\(s :value state).
3026 (\(s :value state).
3028 (Seq (Program (body :value command list))
3030 (\(s :value state).
3032 (One :value state expect))`
3034 ++ `!(s :value state).
3035 (\(s :value state).
3044 (\(s :value state).
3046 (Seq (Program (body :value command list))
3048 (\(s :value state). Int (int_of_value (s i) + (1 :int))))))
3049 (One :value state expect) s`
3051 ++ `(\(s :value state).
3059 (if w = i then Int (0 :int) else (s :value state) w)) <=
3062 (\(s :value state).
3064 (Seq (Program (body :value command list))
3066 (\(s :value state). Int (int_of_value (s i) + (1 :int))))))
3067 (One :value state expect)
3070 ++ Suff `One (s :value state) <=
3071 (\(s :value state).
3187 ``!(i :string) (body :value command) (n :num)
3188 (postE :value state expect).
3189 wp (Assign i (\(s :value state). Int (& n :int)))
3191 (While (\(s :value state). int_of_value (s i) < (& n :int))
3193 wp (Assign i (\(s :value state). Int (& n :int))) postE``,
3195 ++ Q.ABBREV_TAC `g = (\(s :value state).
3197 ++ `wp (While (g :value state -> bool) (body :value command))
3198 (postE :value state expect) =
3199 (\(s :value state).
3202 ++ Q.ABBREV_TAC `foo = (\(s :value state).
3203 (if (g :value state -> bool) s then
3204 wp (body :value command)
3205 (wp (While g body) (postE :value state expect)) s
3216 ``!(body :value command) (i :string) (postE :'a).
3217 (!(postE :value state expect) (m :num).
3218 (\(s :value state).
3220 (\(s :value state).
3229 (\(s :value state).
3231 (\(s :value state).
3240 !(m :num) (n :num) (postE :value state expect).
3242 (wp (Assign i (\(s :value state). Int (& m :int)))
3245 (\(s :value state). int_of_value (s i) < (& n :int))
3248 (\(s :value state).
3251 wp (Assign i (\(s :value state). Int (& m :int)))
3255 (\(s :value state). Int (& (m + (1 :num)) :int)))
3258 (\(s :value state).
3262 (\(s :value state).
3266 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int)))
3268 (While (\(s :value state). int_of_value (s i) < (& (n :num) :int))
3269 (Seq (body :value command)
3271 (\(s :value state).
3273 (postE :value state expect)) =
3274 wp (Assign i (\(s :value state). Int (& m :int)))
3275 (\(s :value state).
3276 (if (\(s :value state). int_of_value (s i) < (& n :int)) s then
3280 (\(s :value state).
3283 (While (\(s :value state). int_of_value (s i) < (& n :int))
3286 (\(s :value state).
3293 (\(s :value state).
3295 (Seq (body :value command)
3297 (\(s :value state). Int (int_of_value (s i) + (1 :int))))))
3298 (postE :value state expect) =
3299 (\(s :value state).
3300 (if (\(s :value state). int_of_value (s i) < (& n :int)) s then
3304 (\(s :value state). Int (int_of_value (s i) + (1 :int)))))
3306 (While (\(s :value state). int_of_value (s i) < (& n :int))
3309 (\(s :value state).
3313 by (Q.ABBREV_TAC `g = (\(s :value state).
3317 (\(s :value state).
3319 (\(s :value state).
3323 (Seq (body :value command)
3325 (\(s :value state).
3329 (\(s :value state).
3333 (\(s :value state).
3335 (postE :value state expect)) s
3347 ``!(n :num) (m :num) (body :value command) (i :string)
3348 (postE :value state expect).
3349 (!(postE :value state expect) (m :num).
3350 (\(s :value state).
3352 (\(s :value state).
3361 (\(s :value state).
3363 (\(s :value state).
3374 (Seq (Assign i (\(s :value state). Int (& m :int)))
3376 (\(s :value state).
3380 (\(s :value state).
3384 (Seq (Assign i (\(s :value state). Int (& m :int)))
3387 (\(s :value state). int_of_value (s i) < (& n :int))
3390 (\(s :value state).
3394 (\(s :value state).
3397 ++ `!(m :num) (n :num) (postE :value state expect).
3399 (wp (Assign (i :string) (\(s :value state). Int (& m :int)))
3401 (While (\(s :value state). int_of_value (s i) < (& n :int))
3402 (Seq (body :value command)
3404 (\(s :value state).
3406 wp (Assign i (\(s :value state). Int (& m :int)))
3408 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int)))
3411 (\(s :value state). int_of_value (s i) < (& n :int))
3414 (\(s :value state).
3418 ++ Q.ABBREV_TAC `loopbody = Seq (body :value command)
3420 (\(s :value state). Int (int_of_value (s i) + (1 :int))))`
3424 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int)))
3426 (While (\(s :value state). int_of_value (s i) < (& (n :num) :int))
3427 (loopbody :value command))
3428 (wp loopbody (postE :value state expect))) =
3429 wp (Assign i (\(s :value state). Int (& m :int))) (wp loopbody postE)`
3434 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int)))
3437 (\(s :value state).
3439 (loopbody :value command)) (postE :value state expect)) =
3440 wp (Assign i (\(s :value state). Int (& m :int)))
3441 (wp (body :value command)
3442 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int)))
3444 by (`wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int)))
3447 (\(s :value state).
3449 (loopbody :value command)) (postE :value state expect)) =
3450 wp (Assign i (\(s :value state). Int (& n :int)))
3451 (wp (body :value command)
3452 (wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int)))
3455 (\(s :value state).
3464 (\(s :value state). Int (& ((n :num) + (1 :num)) :int)))
3467 (\(s :value state).
3469 (loopbody :value command)) (postE :value state expect)) =
3470 wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int))) postE`
3486 (\(s :value state). Int (& (m + (1 :num)) :int)))
3488 (\(s :value state). int_of_value (s i) < (& n :int) + (1 :int))
3489 (loopbody :value command))) (postE :value state expect) =
3491 (Seq (Assign i (\(s :value state). Int (& (m + (1 :num)) :int)))
3493 (While (\(s :value state). int_of_value (s i) < (& n :int))
3499 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int)))
3502 (\(s :value state).
3504 (loopbody :value command)) (postE :value state expect)) =
3505 wp (Assign i (\(s :value state). Int (& m :int)))
3506 (wp (body :value command)
3507 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int)))
3510 (\(s :value state).
3514 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int)))
3517 (\(s :value state).
3519 (loopbody :value command)) (postE :value state expect)) =
3520 wp (Assign i (\(s :value state). Int (& m :int)))
3521 (wp (body :value command)
3522 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int)))
3525 (\(s :value state).
3534 ++ `wp (Assign (i :string) (\(s :value state). Int (& (n :num) :int)))
3537 (\(s :value state).
3539 (loopbody :value command)) (postE :value state expect)) =
3540 wp (Assign i (\(s :value state). Int (& n :int)))
3541 (wp (body :value command)
3542 (wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int)))
3545 (\(s :value state).
3552 (\(s :value state). Int (& ((n :num) + (1 :num)) :int)))
3555 (\(s :value state).
3557 (loopbody :value command)) (postE :value state expect)) =
3558 wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int))) postE`
3563 (\(s :value state).
3565 (loopbody :value command) =
3566 While (\(s :value state). int_of_value (s i) < (& n :int) + (1 :int))
3578 ``!(n :num) (m :num) (body :value command) (i :string)
3579 (postE :value state expect).
3580 (!(postE :value state expect) (m :num).
3581 (\(s :value state).
3583 (\(s :value state).
3592 (\(s :value state).
3594 (\(s :value state).
3605 (For i (\(s :value state). Int (& m :int))
3606 (\(s :value state). int_of_value (s i) < (& (SUC n) :int))
3607 (\(s :value state). Int (int_of_value (s i) + (1 :int)))
3611 (For i (\(s :value state). Int (& m :int))
3612 (\(s :value state). int_of_value (s i) < (& n :int))
3613 (\(s :value state). Int (int_of_value (s i) + (1 :int)))
3617 (\(s :value state).
3624 ``!(n :num) (body :value command) (i :string)
3625 (postE :value state expect).
3626 (!(postE :value state expect) (m :num).
3627 (\(s :value state).
3629 (\(s :value state).
3638 (\(s :value state).
3640 (\(s :value state).
3650 (For i (\(s :value state). Int (0 :int))
3651 (\(s :value state). int_of_value (s i) < (& (SUC n) :int))
3652 (\(s :value state). Int (int_of_value (s i) + (1 :int)))
3656 (For i (\(s :value state). Int (0 :int))
3657 (\(s :value state). int_of_value (s i) < (& n :int))
3658 (\(s :value state). Int (int_of_value (s i) + (1 :int)))
3662 (\(s :value state).