PR# 12837 Repeated postcondition in STRING_8.substring

This postcondition appears in STRING_8:

recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))

Exactly the same appears in STRING_GENERAL. There's no reason for this, is there?

Also, note that first_item appears in both, although the implementation is a bit different. In STRING_GENERAL, first_item ought to be called first_code.

ensure -- from STRING_GENERAL
	substring_not_void: Result /= Void
	substring_count: Result.count = end_index - start_index + 1 or Result.count = 0
	first_item: Result.count > 0 implies Result.code (1) = code (start_index)
	recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))
ensure then
	first_item: Result.count > 0 implies Result.item (1) = item (start_index)
	recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))
end

Thanks for finding this. It will be fixed in the next release. Note that this is now part of FreeELKS.