"""
Cobra supports contracts which are expressed through lists of truthful
expressions attached to objects and methods (and properties). They act as
documentation, specification and run-time assertions.

Cobra's approach to contracts is modeled directly after Eiffel.

Like the other How To's, this program demonstrates language features with
explanatory comments. It is not a practical sample.

Keywords and implicit variables related to contracts include:
	invariant, require, ensure
	result, old, implies
	or require
	and ensure

When a contract condition fails, an exception is raised. The exception message
shows the value of each subexpression in the condition, just like the Cobra
'assert' exception. For example, 'x > y' will show the values of 'x' and 'y'.

You may wish to turn off contracts before shipping software in order to boost
run-time performance and/or reduce executable size. From the command line, you
can turn off contracts with:
	cobra -contracts:none foo.cobra

See also a forum post on contracts:
http://cobra-language.com/forums/viewtopic.php?f=4&t=26
"""

class Entity

	# 'invariant' is followed by a list of truthful expressions
	# These are executed at the end of each code member (initializer, method,
	# property, etc.). They speak to the state of the object.
	invariant
		.serialNum >= 1000
		.name.length > 0
		.actionCount >= 0

	cue init(serialNum as int, name as String)
		require
			serialNum > 0
			name.length > 0
		body
			base.init
			_serialNum = serialNum
			_name = name

	get serialNum from var as int
	
	get name from var as String

	pro isActive from var as bool

	get actionCount from var as int

	def act(ctx as Context)
		require           # Requirements can speak to...
			.isActive     #   the state of the current object
			ctx.isActive  #   the state of the arguments
		ensure
			# Can refer to 'old' values in 'ensure'
			.actionCount == old .actionCount + 1
		body
			_actionCount += 1

	# Properties can have contracts too:
	get upperName as String
		ensure
			# 'result' is an implicit variable in the 'ensure' clause
			result.length == .name.length
		body
			return .name.toUpper


class Context
	"""
	Dummy support class.
	"""

	get isActive as bool
		return true


class Utils

	shared

		def compute(x as float, y as float) as float
			require
				x > 0
				y > 0
			ensure
				result > 0   
			body
				return x.sqrt + y.sqrt

		def normalizeName(name as String) as String
			# If a contract has only one condition, you can write it
			# on one line and skip 'body'.
			require name.trim.length
			ensure result.length <= name.length
			return Utils.capped(name.trim)

		def capped(s as String) as String
			"""
			Returns the string with the first character capitalized.
			Returns a blank string for a blank string.
			"""
			ensure
				result.length == s.length
				result.length implies result[0] == result[0].toUpper
			test
				# Unit tests can enhance contracts by showing example
				# invocations and verifying behavior.
				assert Utils.capped('chuck')=='Chuck'
				assert Utils.capped('Chuck')=='Chuck'
				assert Utils.capped('')==''
				assert Utils.capped(' foo')==' foo'
				assert Utils.capped('f')=='F'
				assert Utils.capped('1aoeu')=='1aoeu'
			body
				if s.length
					return s[0:1].toUpper + s[1:]
				else
					return s


class BaseClass

	def normalizeName(name as String) as String
		require name.trim.length
		return Utils.capped(name.trim)


class DerivedClass inherits BaseClass

	def normalizeName(name as String) as String is override
		# When method contracts are inherited, the 'require' can be weakened 
		# through 'or require' meaning that the DerivedClass is more flexible 
		# about what conditions the work can be done in. The 'ensure' can be 
		# strengthened with 'and ensure' meaning that DerivedClass can 
		# guarantee additional conditions about the results of the work.
		or require
			true   # take any kind of string
		and ensure
			name.trim.length == 0 implies result == '(noname)'
		body
			return Utils.capped(if(name.trim.length, name.trim, '(noname)'))


class Program

	def main is shared
		expect RequireException
			Utils.normalizeName('')  # contract violations throw exceptions
