EiffelStudio Assertions Cheatsheet

Please see the EiffelStudio Assertions Setting blog post for the detailed discussion of the results and the code!

This repository shows which contracts are actually evaluated for different settings in the Assertions group in Project Settings (Project > Project Settings > Target: x > Assertions). The results are presented in the table

	require	check	loop_invariant	loop_variant	ensure	invariant	other_library pre	other_library check	subcluster require	subcluster check	other_cluster pre	other_cluster check	indirect_cluster pre	indirect_cluster check
All	X	X	X	X	X	X	X		X		X
Require	X
Ensure					X
Check		X
Invariant						X
Loop			X	X
Supplier Precondition	X						X		X		X

Rows represent different combinations of assertions enabled. In all examples assertions are enabled only for the main cluster (no prefix):

• All has each assertion option enabled
• other rows have only one respective assertion type enabled: Require enables only the Require option and so on.

Description of other clusters and libraries:

• other_library is a library used directly from the main cluster
• subcluster is a child cluster of the main cluster. As with the other groups in this list, it has all assertions disabled.
• other_cluster is a sibling cluster to the main cluster, directly used by main
• indirect_cluster is another sibling cluster to the main cluster. It is not used directly by main, but other_cluster uses it.

The respective .ecf files are provided in the contract_variants directory, prefixed with check_ (e.g. contract_variants/check_all.ecf).

The table is generated by the run.rb Ruby script. To run it:

bundle install
bundle exec ruby run.rb