-- Calculating the sum of array elements.
-- This example demonstrates logic functions, recursion and sequences.

class
	ARRAY_SUM

feature

	seq_sum (s: MML_SEQUENCE [INTEGER]): INTEGER
			-- Sum of elements in `s'.
			-- (MML_SEQUENCE is a logic class: its objects are mathematical values
			-- and its operations are defined in a Boogie theory).
		note
			status: functional -- This is a logic function (its body acts as a postcondition)
		do
			Result := if s.is_empty then 0 else s.last + seq_sum (s.but_last) end
			-- Try replacing the body with one of the following to test well-formedness checking
--			Result := s.last + seq_sum (s.but_last)
--			Result := if s.is_empty then 0 else s.last + seq_sum (s) end
		end

	array_sum (a: SIMPLE_ARRAY [INTEGER]): INTEGER
			-- Calculate sum of elements in array `a'.
		note
			status: impure -- We do not intend to use this function in contracts
		require
			modify ([]) -- But it doesn't modify existing objects
		local
			i: INTEGER
		do
			from
				i := 1
			invariant
				in_bounds: 1 <= i and i <= a.count + 1
				is_partial_sum: Result = seq_sum (a.sequence.front (i - 1))
			until
				i > a.count
			loop
				check a.sequence.front (i).but_last = a.sequence.front (i - 1) end
				Result := Result + a[i]
				i := i + 1
			end
		ensure
			is_sum: Result = seq_sum (a.sequence)
		end


end