Skip to main content
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
[mdt-ocl.dev] Code synthesis and Pivot/Ecore compatibility 
Hi
After too much documentation, I felt like a play, so I took at shot at the Acceleo OCL Code generator; a WIP is attached as a teaser. About 300 Acceleo lines and it's looking remarkably functional.
The vague goal is to match the UML genmodel Operations classes so that integration with genmodel can occur mostly in *.operations classes hopefully leaving *.impl unchanged.
Anyway, I'm amazed how easy it is and that iterations present no significant problems. It will not be necessary to have an OCL subset for which Java code generation is possible.
Optimisation. The example has no optimisation; the aim is to demonstrate that all analysis and much of the scheduling can be done at compile time. The AST is actually quite good for code generation, so it may be that optimisation just annotates the tree (perhaps using adapters) with knowledge such as operation-is-final, known-type-numeric-bounds, known-value-non-nullness, known-value-non-invalidity, folded-constants. This could be extensible without needing more AST variants. 

At the heart of the code gen are two kernel facilities
dispatch an operation/iteration
navigate a property/value acquisition
Operation dispatch is where things can get really slow because of the need to perform type conformance tests. If this is done on the Pivot/Ecore metamodel, it is horribly slow for multiple level of hierarchy ultimately terminating in OclAny. So if we're aiming at fast code execution we should have an optimized data structure for dispatch (cf. C++ virtual function tables). Since this would be at the implementation rather than modeling level, it would be neither Pivot nor Ecore and so would be easy to create from either. It may therefore be possible to push the Pivot/Ecore compatibility issue to the far side of oclType().
Property navigation is naively an eGet on an EObject (the Pivot evaluator has to do a Pivot to Ecore lookup to get the EReference). This is also a value acquisition and so requires the external to Value conversion to be performed.
Similarly on return, an Ecore API, must perform Value to external representation conversion.
It is the uniform polymorphism of Value that makes this all so easy. If we can push the Pivot/Ecore issue behind oclType(), it should be possible to avoid any Pivot overheads for the common use case of load and use pre-compiled models. NB. the attached uses only pivot Value classes and InvalidValueException, no pivot model classes at all; they're all hidden by the monikers that uniquely identify model objects.
Axel: It would be good to discuss how you might like to proceed with this in Zurich.
Perhaps you have a student who would like to study fast virtual function dispatch tables for models. 

    Regards

        Ed



package test;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import org.eclipse.ocl.examples.pivot.InvalidValueException;
import org.eclipse.ocl.examples.pivot.values.*;

@SuppressWarnings("unused")
public class FirstClassOperations
{
	/**
	 *	The model interaction API.
     */
	public abstract static class CodeGenImplementation 
	{
		public Value dispatch(Value source, String operationMoniker, Value... arguments) throws InvalidValueException {
			return null;		// TODO implement me
		}
		public Value dispatch(Value source, String iterationMoniker, Value initial, CodeGenImplementation body) throws InvalidValueException {
			return null;		// TODO implement me
		}
		public abstract Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException;
		public Value navigate(Value source, String propertyMoniker) {
			return null;		// TODO implement me
		}
		public Value tupleFor(String tupleMoniker, Map<String, Value> partMap) {
			return null;		// TODO implement me
		}
		public Value typeOf(String typeMoniker) {
			return null;		// TODO implement me
		}
	}

	public static void suppressThrowWarnings()  throws InvalidValueException {}


	/** 
	 * Implementation of the FirstClass 'binary' invariant.
	 *
	 * true.or(false)
	 */
	public static class FirstClass_inv_binary extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_1 = sourceValue;		// self
			Value symbol_2;
			try {
				suppressThrowWarnings();
				symbol_2 = valueFactory.booleanValueOf(true);
			} catch (InvalidValueException e) {
				symbol_2 = valueFactory.getInvalid();
			}
			Value symbol_3;
			try {
				suppressThrowWarnings();
				symbol_3 = valueFactory.booleanValueOf(false);
			} catch (InvalidValueException e) {
				symbol_3 = valueFactory.getInvalid();
			}
			Value result = dispatch(symbol_2, "Boolean!or(Boolean)", symbol_3);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'constant' invariant.
	 *
	 * true
	 */
	public static class FirstClass_inv_constant extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_4 = sourceValue;		// self
			Value result = valueFactory.booleanValueOf(true);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'if' invariant.
	 *
	 * if true then 'x' else 'y' endif
	 */
	public static class FirstClass_inv_if extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_5 = sourceValue;		// self
			Value result_symbol_6;
			Value if_symbol_6 = valueFactory.booleanValueOf(true);
			if (if_symbol_6.isTrue()) {
				result_symbol_6 = valueFactory.stringValueOf("x");
			}
			else if (if_symbol_6.isFalse()) {
				result_symbol_6 = valueFactory.stringValueOf("y");
			}
			else if (if_symbol_6.isNull()) {
				result_symbol_6 = valueFactory.throwInvalidValueException("null if condition");
			}
			else {
				result_symbol_6 = valueFactory.throwInvalidValueException("invalid if condition");
			}
			Value result = result_symbol_6;
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'let' invariant.
	 *
	 * let x : Boolean = true in x
	 */
	public static class FirstClass_inv_let extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_7 = sourceValue;		// self
			final Value symbol_8 = valueFactory.booleanValueOf(true);
			Value result = symbol_8;
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'loop' invariant.
	 *
	 * Sequence {1}->exists(e : Integer | e.=('xyzzy'))
	 */
	public static class FirstClass_inv_loop extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_9 = sourceValue;		// self
			List<Value> list_symbol_10 = new ArrayList<Value>(); 
			Value item_symbol_12 = valueFactory.integerValueOf(1);
			list_symbol_10.add(item_symbol_12);
			Value symbol_10 = valueFactory.createCollectionValue(org.eclipse.ocl.examples.pivot.CollectionKind.SEQUENCE, list_symbol_10);
			
			/** 
			 * Implementation of the iterator body.
			 *
			 * e.=('xyzzy')
			 */
			CodeGenImplementation body_symbol_11 = new CodeGenImplementation()
			{
				public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
					Value symbol_13 = argValues[0];	// iterator: e
					Value symbol_14 = symbol_13;
					Value symbol_15 = valueFactory.stringValueOf("xyzzy");
					Value result = dispatch(symbol_14, "$ocl!OclAny!=($ocl!OclSelf)", symbol_15);
					return result;
				}
			};
			Value result = dispatch(symbol_10, "$ocl!Collection{T}!exists(T|Lambda~T()Boolean)", null, body_symbol_11);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'maths' invariant.
	 *
	 * 1.+(2.*(3.0)./(4))
	 */
	public static class FirstClass_inv_maths extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_16 = sourceValue;		// self
			Value symbol_17 = valueFactory.integerValueOf(1);
			Value symbol_20 = valueFactory.integerValueOf(2);
			Value symbol_21 = valueFactory.realValueOf(3.0);
			Value symbol_19 = dispatch(symbol_20, "Real!*($ocl!OclSelf)", symbol_21);
			Value symbol_22 = valueFactory.integerValueOf(4);
			Value symbol_18 = dispatch(symbol_19, "Real!/($ocl!OclSelf)", symbol_22);
			Value result = dispatch(symbol_17, "Real!+($ocl!OclSelf)", symbol_18);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'nested' invariant.
	 *
	 * let outer : String = 'outer' in outer.oclAsSet()->iterate(s : String; acc : String = 'a' | let inner : String = 'inner' in inner.oclAsSet()->iterate(s : String; acc : String = 'b' | acc.+('_').+(s).+('
	').+(outer).+('ᄑ').+(inner)))
	 */
	public static class FirstClass_inv_nested extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_23 = sourceValue;		// self
			final Value symbol_24 = valueFactory.stringValueOf("outer");
			Value symbol_28 = symbol_24;
			Value symbol_25 = dispatch(symbol_28, "$ocl!OclAny!oclAsSet()");
			Value symbol_26 = valueFactory.stringValueOf("a");
			
			/** 
			 * Implementation of the iterate body.
			 *
			 * let inner : String = 'inner' in inner.oclAsSet()->iterate(s : String; acc : String = 'b' | acc.+('_').+(s).+('
			').+(outer).+('ᄑ').+(inner))
			 */
			CodeGenImplementation body_symbol_27 = new CodeGenImplementation()
			{
				public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
					Value symbol_26 = sourceValue;	// accumulator: acc
					Value symbol_29 = argValues[0];	// iterator: s
					final Value symbol_30 = valueFactory.stringValueOf("inner");
					Value symbol_34 = symbol_30;
					Value symbol_31 = dispatch(symbol_34, "$ocl!OclAny!oclAsSet()");
					Value symbol_32 = valueFactory.stringValueOf("b");
					
					/** 
					 * Implementation of the iterate body.
					 *
					 * acc.+('_').+(s).+('
					').+(outer).+('ᄑ').+(inner)
					 */
					CodeGenImplementation body_symbol_33 = new CodeGenImplementation()
					{
						public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
							Value symbol_32 = sourceValue;	// accumulator: acc
							Value symbol_35 = argValues[0];	// iterator: s
							Value symbol_41 = symbol_32;
							Value symbol_42 = valueFactory.stringValueOf("_");
							Value symbol_40 = dispatch(symbol_41, "String!+(String)", symbol_42);
							Value symbol_43 = symbol_35;
							Value symbol_39 = dispatch(symbol_40, "String!+(String)", symbol_43);
							Value symbol_44 = valueFactory.stringValueOf("\n");
							Value symbol_38 = dispatch(symbol_39, "String!+(String)", symbol_44);
							Value symbol_45 = symbol_24;
							Value symbol_37 = dispatch(symbol_38, "String!+(String)", symbol_45);
							Value symbol_46 = valueFactory.stringValueOf("\u1111");
							Value symbol_36 = dispatch(symbol_37, "String!+(String)", symbol_46);
							Value symbol_47 = symbol_30;
							Value result = dispatch(symbol_36, "String!+(String)", symbol_47);
							return result;
						}
					};
					Value result = dispatch(symbol_31, "$ocl!Collection{T}!iterate{Tacc}(T;Tacc)", symbol_32, body_symbol_33);
					return result;
				}
			};
			Value result = dispatch(symbol_25, "$ocl!Collection{T}!iterate{Tacc}(T;Tacc)", symbol_26, body_symbol_27);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'product' invariant.
	 *
	 * Bag {3, 4}->product(OrderedSet {3.0, 4.0}).=(Set {Tuple{first : UnlimitedNatural = 3, second : Real = 3.0}, Tuple{first : UnlimitedNatural = 3, second : Real = 4.0}, Tuple{first : UnlimitedNatural = 4, second : Real = 3.0}, Tuple{first : UnlimitedNatural = 4, second : Real = 4.0}})
	 */
	public static class FirstClass_inv_product extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_48 = sourceValue;		// self
			List<Value> list_symbol_50 = new ArrayList<Value>(); 
			Value item_symbol_51 = valueFactory.integerValueOf(3);
			list_symbol_50.add(item_symbol_51);
			Value item_symbol_52 = valueFactory.integerValueOf(4);
			list_symbol_50.add(item_symbol_52);
			Value symbol_50 = valueFactory.createCollectionValue(org.eclipse.ocl.examples.pivot.CollectionKind.BAG, list_symbol_50);
			List<Value> list_symbol_53 = new ArrayList<Value>(); 
			Value item_symbol_54 = valueFactory.realValueOf(3.0);
			list_symbol_53.add(item_symbol_54);
			Value item_symbol_55 = valueFactory.realValueOf(4.0);
			list_symbol_53.add(item_symbol_55);
			Value symbol_53 = valueFactory.createCollectionValue(org.eclipse.ocl.examples.pivot.CollectionKind.ORDERED_SET, list_symbol_53);
			Value symbol_49 = dispatch(symbol_50, "$ocl!Collection{T}!product{T2}($ocl!Collection[T2])", symbol_53);
			List<Value> list_symbol_56 = new ArrayList<Value>(); 
			Map<String, Value> symbol_58 = new HashMap<String, Value>();
			Value symbol_59 = valueFactory.integerValueOf(3);
			symbol_58.put("first", symbol_59);
			Value symbol_60 = valueFactory.realValueOf(3.0);
			symbol_58.put("second", symbol_60);
			Value item_symbol_57 = tupleFor("Tuple{first:UnlimitedNatural,second:Real}", symbol_58);
			list_symbol_56.add(item_symbol_57);
			Map<String, Value> symbol_62 = new HashMap<String, Value>();
			Value symbol_63 = valueFactory.integerValueOf(3);
			symbol_62.put("first", symbol_63);
			Value symbol_64 = valueFactory.realValueOf(4.0);
			symbol_62.put("second", symbol_64);
			Value item_symbol_61 = tupleFor("Tuple{first:UnlimitedNatural,second:Real}", symbol_62);
			list_symbol_56.add(item_symbol_61);
			Map<String, Value> symbol_66 = new HashMap<String, Value>();
			Value symbol_67 = valueFactory.integerValueOf(4);
			symbol_66.put("first", symbol_67);
			Value symbol_68 = valueFactory.realValueOf(3.0);
			symbol_66.put("second", symbol_68);
			Value item_symbol_65 = tupleFor("Tuple{first:UnlimitedNatural,second:Real}", symbol_66);
			list_symbol_56.add(item_symbol_65);
			Map<String, Value> symbol_70 = new HashMap<String, Value>();
			Value symbol_71 = valueFactory.integerValueOf(4);
			symbol_70.put("first", symbol_71);
			Value symbol_72 = valueFactory.realValueOf(4.0);
			symbol_70.put("second", symbol_72);
			Value item_symbol_69 = tupleFor("Tuple{first:UnlimitedNatural,second:Real}", symbol_70);
			list_symbol_56.add(item_symbol_69);
			Value symbol_56 = valueFactory.createCollectionValue(org.eclipse.ocl.examples.pivot.CollectionKind.SET, list_symbol_56);
			Value result = dispatch(symbol_49, "$ocl!OclAny!=($ocl!OclSelf)", symbol_56);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'set' invariant.
	 *
	 * Set {1, 2, 3, 5 .. 7, 8, 10 .. 6}
	 */
	public static class FirstClass_inv_set extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_73 = sourceValue;		// self
			List<Value> list_symbol_74 = new ArrayList<Value>(); 
			Value item_symbol_75 = valueFactory.integerValueOf(1);
			list_symbol_74.add(item_symbol_75);
			Value item_symbol_76 = valueFactory.integerValueOf(2);
			list_symbol_74.add(item_symbol_76);
			Value item_symbol_77 = valueFactory.integerValueOf(3);
			list_symbol_74.add(item_symbol_77);
			IntegerValue first_symbol_78 = valueFactory.integerValueOf(5);
			IntegerValue last_symbol_78 = valueFactory.integerValueOf(7);
			int start_symbol_78 = first_symbol_78.asInteger();
			int end_symbol_78 = last_symbol_78.asInteger();
			int delta_symbol_78 = start_symbol_78 > end_symbol_78 ? -1 :1;
			list_symbol_74.add(first_symbol_78);
			for (int symbol_78 = start_symbol_78; symbol_78 != end_symbol_78; symbol_78 += delta_symbol_78) {
				list_symbol_74.add(valueFactory.integerValueOf(symbol_78));
			}
			Value item_symbol_79 = valueFactory.integerValueOf(8);
			list_symbol_74.add(item_symbol_79);
			IntegerValue first_symbol_80 = valueFactory.integerValueOf(10);
			IntegerValue last_symbol_80 = valueFactory.integerValueOf(6);
			int start_symbol_80 = first_symbol_80.asInteger();
			int end_symbol_80 = last_symbol_80.asInteger();
			int delta_symbol_80 = start_symbol_80 > end_symbol_80 ? -1 :1;
			list_symbol_74.add(first_symbol_80);
			for (int symbol_80 = start_symbol_80; symbol_80 != end_symbol_80; symbol_80 += delta_symbol_80) {
				list_symbol_74.add(valueFactory.integerValueOf(symbol_80));
			}
			Value result = valueFactory.createCollectionValue(org.eclipse.ocl.examples.pivot.CollectionKind.SET, list_symbol_74);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'set2' invariant.
	 *
	 * Set {1, 2, 3}->size().=(3)
	 */
	public static class FirstClass_inv_set2 extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_81 = sourceValue;		// self
			List<Value> list_symbol_83 = new ArrayList<Value>(); 
			Value item_symbol_84 = valueFactory.integerValueOf(1);
			list_symbol_83.add(item_symbol_84);
			Value item_symbol_85 = valueFactory.integerValueOf(2);
			list_symbol_83.add(item_symbol_85);
			Value item_symbol_86 = valueFactory.integerValueOf(3);
			list_symbol_83.add(item_symbol_86);
			Value symbol_83 = valueFactory.createCollectionValue(org.eclipse.ocl.examples.pivot.CollectionKind.SET, list_symbol_83);
			Value symbol_82 = dispatch(symbol_83, "$ocl!Collection{T}!size()");
			Value symbol_87 = valueFactory.integerValueOf(3);
			Value result = dispatch(symbol_82, "Real!=($ocl!OclSelf)", symbol_87);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'type' invariant.
	 *
	 * if self.oclIsKindOf(ocl::Integer) then self.oclAsType(ocl::Integer) else invalid endif
	 */
	public static class FirstClass_inv_type extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_88 = sourceValue;		// self
			Value result_symbol_89;
			Value symbol_90 = symbol_88;
			Value symbol_91 = typeOf("Integer");
			Value if_symbol_89 = dispatch(symbol_90, "$ocl!OclAny!oclIsKindOf{T}($ocl!Classifier[T])", symbol_91);
			if (if_symbol_89.isTrue()) {
				Value symbol_92 = symbol_88;
				Value symbol_93 = typeOf("Integer");
				result_symbol_89 = dispatch(symbol_92, "$ocl!OclAny!oclAsType{TT}($ocl!Classifier[TT])", symbol_93);
			}
			else if (if_symbol_89.isFalse()) {
				result_symbol_89 = valueFactory.throwInvalidValueException("invalid literal");
			}
			else if (if_symbol_89.isNull()) {
				result_symbol_89 = valueFactory.throwInvalidValueException("null if condition");
			}
			else {
				result_symbol_89 = valueFactory.throwInvalidValueException("invalid if condition");
			}
			Value result = result_symbol_89;
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass 'var' invariant.
	 *
	 * self.s.+('*').+(self.s)
	 */
	public static class FirstClass_inv_var extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_94 = sourceValue;		// self
			Value symbol_97 = symbol_94;
			Value symbol_96 = navigate(symbol_97, "test!FirstClass!s");
			Value symbol_98 = valueFactory.stringValueOf("*");
			Value symbol_95 = dispatch(symbol_96, "String!+(String)", symbol_98);
			Value symbol_100 = symbol_94;
			Value symbol_99 = navigate(symbol_100, "test!FirstClass!s");
			Value result = dispatch(symbol_95, "String!+(String)", symbol_99);
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass::caseInvert '' <body>.
	 *
	 * if b then false else true endif
	 */
	public static class FirstClass_caseInvert_body_ extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_101 = sourceValue;		// self
			Value symbol_102 = argValues[0];	// parameter: b
			Value result_symbol_103;
			Value if_symbol_103 = symbol_102;
			if (if_symbol_103.isTrue()) {
				result_symbol_103 = valueFactory.booleanValueOf(false);
			}
			else if (if_symbol_103.isFalse()) {
				result_symbol_103 = valueFactory.booleanValueOf(true);
			}
			else if (if_symbol_103.isNull()) {
				result_symbol_103 = valueFactory.throwInvalidValueException("null if condition");
			}
			else {
				result_symbol_103 = valueFactory.throwInvalidValueException("invalid if condition");
			}
			Value result = result_symbol_103;
			return result;
		}
	}

	/** 
	 * Implementation of the FirstClass::s '' <derivation>.
	 *
	 * 1.+(2).+(3)
	 */
	public static class FirstClass_s_derivation_ extends CodeGenImplementation
	{
		public Value evaluate(ValueFactory valueFactory, Value sourceValue, Value... argValues) throws InvalidValueException {
			Value symbol_104 = sourceValue;		// self
			Value symbol_106 = valueFactory.integerValueOf(1);
			Value symbol_107 = valueFactory.integerValueOf(2);
			Value symbol_105 = dispatch(symbol_106, "Integer!+($ocl!OclSelf)", symbol_107);
			Value symbol_108 = valueFactory.integerValueOf(3);
			Value result = dispatch(symbol_105, "Integer!+($ocl!OclSelf)", symbol_108);
			return result;
		}
	}
}

package test : pfx = 'platform:/resource/org.eclipse.ocl.examples.build/test/model/test.oclinecore'
{
	class FirstClass
	{
		invariant constant: true;
		invariant binary: true or false;
		invariant maths: 1 + 2 * 3.0 / 4;
		invariant set: Set{1,2,3,5..7,8,10..6};
		invariant set2: Set<Integer>{1,2,3}->size() = 3;
		invariant loop: Sequence{1}->exists(e : Integer | e = 'xyzzy');
		invariant var: self.s + '*' + self.s;
		invariant type: if self.oclIsKindOf(Integer) then self.oclAsType(Integer) else invalid endif;
		invariant _'let': let x : Boolean = true in x;
		invariant _'if': if true then 'x' else 'y' endif;
		invariant nested: 
			let outer : String = 'outer'
			in outer->iterate(s : String; acc : String = 'a' |
				let inner : String = 'inner'
				in inner->iterate(s : String; acc : String = 'b' |
					acc + '_' + s + '\n' + outer + '\u1111' + inner));
		invariant product: Bag{3, 4}->product(OrderedSet{3.0, 4.0}) = Set{Tuple{first = 3, second = 3.0}, Tuple{first = 3, second = 4.0}, Tuple{first = 4, second = 3.0}, Tuple{first = 4, second = 4.0}};		
		
		operation caseInvert(b : Boolean) : Boolean {
			body: if b then false else true endif; 
		}
		
		property s : String {
			derivation: 1 + 2 + 3;
		}
	}
}

Back to the top