isabelle: src/HOL/IMP/Abs_Int_Tests.thy@8262d4f63b58 (annotated)

68778 4566bac4517d improved sectioning nipkow parents: 67406 diff changeset	1	(* Author: Tobias Nipkow *)
4566bac4517d improved sectioning nipkow parents: 67406 diff changeset	2
4566bac4517d improved sectioning nipkow parents: 67406 diff changeset	3	subsection "Abstract Interpretation Test Programs"
4566bac4517d improved sectioning nipkow parents: 67406 diff changeset	4
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	5	theory Abs_Int_Tests
49095 7df19036392e added annotations after condition in if and while nipkow parents: 46432 diff changeset	6	imports Com
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	7	begin
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	8
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	9	text\<open>For constant propagation:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	10
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	11	text\<open>Straight line code:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	12	definition "test1_const =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	13	''y'' ::= N 7;;
bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	14	''z'' ::= Plus (V ''y'') (N 2);;
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	15	''y'' ::= Plus (V ''x'') (N 0)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	16
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	17	text\<open>Conditional:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	18	definition "test2_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	19	IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	20
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	21	text\<open>Conditional, test is relevant:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	22	definition "test3_const =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	23	''x'' ::= N 42;;
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	24	IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	25
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	26	text\<open>While:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	27	definition "test4_const =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	28	''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	29
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	30	text\<open>While, test is relevant:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	31	definition "test5_const =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	32	''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	33
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	34	text\<open>Iteration is needed:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	35	definition "test6_const =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	36	''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	37	WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	38
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58410 diff changeset	39	text\<open>For intervals:\<close>
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	40
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	41	definition "test1_ivl =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	42	''y'' ::= N 7;;
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	43	IF Less (V ''x'') (V ''y'')
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	44	THEN ''y'' ::= Plus (V ''y'') (V ''x'')
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	45	ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	46
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	47	definition "test2_ivl =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	48	WHILE Less (V ''x'') (N 100)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	49	DO ''x'' ::= Plus (V ''x'') (N 1)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	50
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	51	definition "test3_ivl =
52107 0c21dffc177a tuned nipkow parents: 52046 diff changeset	52	''x'' ::= N 0;;
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	53	WHILE Less (V ''x'') (N 100)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	54	DO ''x'' ::= Plus (V ''x'') (N 1)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	55
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	56	definition "test4_ivl =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	57	''x'' ::= N 0;; ''y'' ::= N 0;;
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	58	WHILE Less (V ''x'') (N 11)
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	59	DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N 1))"
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	60
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	61	definition "test5_ivl =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	62	''x'' ::= N 0;; ''y'' ::= N 0;;
52107 0c21dffc177a tuned nipkow parents: 52046 diff changeset	63	WHILE Less (V ''x'') (N 100)
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	64	DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	65
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	66	definition "test6_ivl =
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 51922 diff changeset	67	''x'' ::= N 0;;
58410 6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum haftmann parents: 52107 diff changeset	68	WHILE Less (N (- 1)) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
45623 f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	69
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs, nipkow parents: diff changeset	70	end

author	paulson
	Wed, 17 Apr 2024 22:07:21 +0100
changeset 80130	8262d4f63b58
parent 68778	4566bac4517d
permissions	-rw-r--r--