INForum 2024

Installation & Configuration

To install both Cameleer and Gospel, one should use a specific branch of a fork. Start by cloning Cameleer and Gospel, and checkout to the origin/iteration branch on both forks.

I recommend making a new opam switch (naming it inforum, for example) with the 4.14.0 base compiler:

opam switch inforum 4.14.0
eval $(opam env --switch=inforum)

Then, one should first install Gospel and Cameleer (on the origin/iteration branches), with the following command in both directories:

opam pin add . kind=path
eval $(opam env)

If everything was successful, one should now be able to run cameleer.

Code and Specification

A zip with the full list of examples can be found here. One strategy that can be used, in Why3, is to select a Verification Condition or Module and press R, this will re-run the saved session.

Statistics (Per Module)

Seq

Obligations		Alt-Ergo 2.5.2	Z3 4.12.4
List.S.Fold.permitted_empty		0.05	---
List.S.Iter.permitted_empty		0.05	---
VC for sum_of_seq		---	---
split_vc
	loop invariant init	0.09	---
	precondition	0.09	---
	precondition	0.07	---
	loop variant decrease	0.09	---
	loop invariant preservation	8.30	---
	postcondition	---	0.30
VC for queue_of_seq		0.50	---
VC for noccs_of_seq		---	0.45
VC for max_of_seq		---	0.15
VC for stack_of_seq		2.26	---

Oper

Obligations			Alt-Ergo 2.5.2	CVC4 1.7
equal_hashes_COMPARABLE			0.07	---
VC for gt			---	---
exists (empty1: fset t)
	gt'vc.0		---	---
	exists ( fun(_: t) -> empty1: fset t)
		gt'vc.0.0	0.06	---
Oper.G.Fold_vertex.permitted_empty			0.08	---
Oper.G.Fold_succ.permitted_empty			0.07	---
Oper.G.Fold_succ_e.permitted_empty			0.09	---
Oper.G.Fold_edges.permitted_empty			0.08	---
VC for copy_vertices			---	---
split_vc
	loop invariant init		0.09	---
	precondition		0.08	---
	precondition		0.07	---
	loop variant decrease		0.11	---
	loop invariant preservation		0.27	---
	postcondition		0.10	---
	postcondition		0.07	---
VC for intersect			---	---
split_vc
	loop invariant init		0.12	---
	precondition		0.09	---
	precondition		0.07	---
	loop invariant init		0.84	---
	precondition		0.11	---
	precondition		0.08	---
	loop variant decrease		0.17	---
	loop invariant preservation		---	---
	split_vc
		loop invariant preservation	1.05	---
		loop invariant preservation	0.98	---
	loop variant decrease		0.19	---
	loop invariant preservation		0.19	---
	loop variant decrease		0.15	---
	loop invariant preservation		0.51	---
	postcondition		0.24	---
	postcondition		0.12	---
VC for mirror			---	---
split_vc
	loop invariant init		0.15	---
	precondition		0.10	---
	precondition		0.10	---
	loop variant decrease		0.10	---
	loop invariant preservation		---	1.32
	postcondition		0.16	---
	postcondition		0.11	---
VC for complement			---	---
split_vc
	loop invariant init		0.40	---
	precondition		0.08	---
	precondition		0.08	---
	loop invariant init		1.47	---
	precondition		0.09	---
	precondition		0.09	---
	loop variant decrease		0.16	---
	loop invariant preservation		---	---
	split_vc
		loop invariant preservation	1.12	---
		loop invariant preservation	4.26	---
	loop variant decrease		0.20	---
	loop invariant preservation		0.47	---
	postcondition		0.13	---
	postcondition		0.09	---
	postcondition		0.11	---
VC for union			---	---
split_vc
	loop invariant init		0.24	---
	precondition		0.08	---
	precondition		0.08	---
	loop invariant init		1.65	---
	precondition		0.09	---
	precondition		0.08	---
	loop variant decrease		0.18	---
	loop invariant preservation		---	---
	split_vc
		loop invariant preservation	---	2.41
	loop variant decrease		0.24	---
	loop invariant preservation		0.37	---
	postcondition		0.09	---
	postcondition		---	0.62

Path

Obligations																Alt-Ergo 2.5.2	CVC4 1.7
seq_cons																0.04	---
equal_hashes_HASHABLE																0.04	---
equal_hashes_COMPARABLE																0.04	---
VC for gt																---	---
exists (empty1: fset t)
	gt'vc.0															---	---
	exists (fun(_:t) -> empty1: fset t)
		gt'vc.0.0														0.06	---
Check.G.Iter_succ.permitted_empty																0.04	---
Check.path_suc																---	---
split_vc
	path_suc.0															---	---
	unfold has_path
		path_suc.0.0														---	---
		unfold has_path in H1
			path_suc.0.0.0													---	---
			introduce_exists
				path_suc.0.0.0.0												---	---
				exists (snoc p v3)
					path_suc.0.0.0.0.0											0.11	---
Check.edge_path																0.06	---
Check.self_path																0.10	---
VC for intermediate_value_func																2.67	---
Check.intermediate_value																---	---
split_vc
	intermediate_value.0															---	---
	instantiate intermediate_value_func'spec p,u,v
		intermediate_value.0.0														---	---
		instantiate Hinst (to_list s)
			intermediate_value.0.0.0													---	---
			instantiate Hinst g
				intermediate_value.0.0.0.0												---	---
				destruct_rec Hinst
					destruct premise											0.04	---
					destruct premise											0.05	---
					destruct premise											0.25	---
					intermediate_value.0.0.0.0.3											0.44	---
VC for check_path																---	---
split_vc
	postcondition															0.08	---
	postcondition															0.08	---
	postcondition															0.08	---
	postcondition															0.05	---
	postcondition															0.05	---
	postcondition															0.06	---
	postcondition															0.08	---
	postcondition															0.06	---
	postcondition															0.07	---
	postcondition															0.09	---
	postcondition															0.08	---
	postcondition															0.06	---
	postcondition															0.14	---
	postcondition															0.37	---
	postcondition															1.91	---
	postcondition															0.09	---
	postcondition															0.08	---
	postcondition															0.11	---
	postcondition															0.08	---
	postcondition															---	---
	unfold disjoint
		VC for check_path														2.20	---
	postcondition															0.10	---
	postcondition															0.14	---
	postcondition															0.52	---
	postcondition															0.09	---
	precondition															0.35	---
	loop invariant init															---	---
	split_vc
		loop invariant init														---	---
		inline_goal
			loop invariant init													---	---
			split_all_full
				VC for check_path												0.11	---
				VC for check_path												0.54	---
				VC for check_path												0.11	---
				VC for check_path												1.32	---
				split_vc
					VC for check_path											1.32	---
				VC for check_path												0.10	---
				VC for check_path												0.13	---
				VC for check_path												---	---
				unfold disjoint
					VC for check_path											---	---
					split_vc
						VC for check_path										0.86	---
						VC for check_path										0.93	---
				VC for check_path												0.12	---
				VC for check_path												0.78	---
				VC for check_path												0.09	---
				VC for check_path												0.09	---
				VC for check_path												0.09	---
				VC for check_path												---	---
				inline_goal
					VC for check_path											0.11	---
	precondition															0.11	---
	precondition															0.10	---
	loop variant decrease															0.42	---
	loop invariant preservation															---	---
	split_vc
		loop invariant preservation														---	---
		inline_goal
			loop invariant preservation													---	---
			split_all_full
			VC for check_path												0.08	---
			VC for check_path												1.01	---
			VC for check_path												---	---
			split_vc
				VC for check_path											---	---
				inline_goal
					VC for check_path										---	12.84
			VC for check_path												0.50	---
			VC for check_path												4.52	---
			VC for check_path												0.45	---
			VC for check_path												5.02	---
			VC for check_path												0.17	---
			VC for check_path												0.46	---
			VC for check_path												0.08	---
			VC for check_path												0.11	---
			VC for check_path												0.18	---
			VC for check_path												0.82	---
loop variant decrease															0.47	---
loop invariant preservation															1.28	---
variant decrease															0.37	---
precondition															---	---
case (mem3 v1 q.view2)
	true case (precondition)														0.09	---
	false case (precondition)														---	---
	case (mem3 v2 q.view2)
		false case (true case. precondition)													0.34	---
		false case (precondition)													---	---
		assert (not mem1 v2 visited.dom)
			asserted formula												0.06	---
			false case (precondition)												---	---
			assert (mem1 v1 visited.dom)
				asserted formula											0.08	---
				false case (precondition)											---	---
				instantiate intermediate_value (fun x -> mem1 x visited.dom)
					false case (precondition)										---	---
					instantiate Hinst v1,v2
						false case (precondition)									---	---
						unfold has_path in H
							false case (precondition)								---	---
							introduce_exists
								false case (precondition)							---	---
								instantiate Hinst p,graph
									false case (precondition)						---	---
									destruct Hinst
										destruct premise					0.07	---
										false case (precondition)					---	---
										destruct Hinst
											destruct premise				0.07	---
											false case (precondition)				---	---
											destruct Hinst
												destruct premise			0.06	---
												false case (precondition)			---	---
												introduce_exists
													false case (precondition)		---	---
													exists v'
														check_path'vc.33.1.1.1.1.0.0.0.0.0.1.1.1.0.0	1.70	---
precondition															0.10	---
precondition															0.19	---
precondition															0.36	---
precondition															---	---
assert (forall vt. mem4 vt sucs -> mem1 vt graph.dom1)
	asserted formula														0.10	---
	precondition														0.09	---
precondition															0.10	---
precondition															0.11	---
precondition															0.11	---
precondition															0.17	---
precondition															---	---
split_vc
	precondition														0.40	---
precondition															0.16	---
precondition															0.17	---
precondition															0.08	---
postcondition															0.10	---
postcondition															0.10	---
postcondition															0.10	---
postcondition															0.08	---
postcondition															0.09	---
postcondition															0.12	---
postcondition															0.10	---
postcondition															0.09	---
postcondition															0.11	---
postcondition															0.29	---
postcondition															0.12	---
postcondition															0.10	---
exceptional postcondition															0.09	---
precondition															0.11	---
precondition															0.11	---
precondition															0.11	---
precondition															0.18	---
precondition															0.19	---
precondition															0.20	---
precondition															0.23	---
precondition															0.41	---
precondition															0.11	---
precondition															0.23	---
precondition															0.12	---
precondition															0.16	---
precondition															0.09	---
postcondition															0.08	---

Tree

Obligations		Alt-Ergo 2.5.2
Tree.T.Fold.permitted_empty		0.06
Tree.T.Fold_level.permitted_empty		0.07
Tree.T.Iter.permitted_empty		0.05
VC for sum_tree		---
split_vc
	loop invariant init	0.06
	precondition	0.08
	precondition	0.05
	loop variant decrease	0.08
	loop invariant preservation	15.34
VC for tree_height		0.08

Platform used

The benchmarks were conducted on a machine with a processor i5-2520M 2 cores @ 3.2GHz; 12Gb RAM; 64-bit linux kernel 6.9.5.