simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements; simplified check_specification, read_specification: operate on a single list of simultaneous statements; tuned;