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

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

author	paulson
	Tue, 15 Aug 2017 22:22:34 +0100
changeset 66440	a6ec6c806a6c
parent 58410	6d46ad54a2ab
child 67406	23307fd33906
permissions	-rw-r--r--