Summary: Specification semantics for parallel loop execution.

Given a C# loop such as

		 foreach (int i in intArray.Count)
		 {
	

intArrayi += 3;

		 }
	

(i.e. where iteration X is independent of iteration Y) it would be beneficial to have a means for specifying that the iterations can be done in parallel. This may be a simple extension of the forall construct already intended for use in specifications:

		 forall (int i in intArray.Count)
		 {
	

intArrayi += 3;

		 }
	

The distinction between forall and foreach would then be a requirement that execution of the body of a forall construct be independent of everyother execution of that loop body.

Therefore, the following would be invalid:

		 int sum = 0;
		 forall (int i in intArray.Count)
		 {
		 	sum += intArray[i]; // okay for parallel
		 	if (i > 0)
		 	{
		 		// Now smooth values
		 		intArray[i] = (intArray[i-1] + intArray[i]) / 2; // not ok
		 	}
		 }
	

For extra credit, Spec# could notify the user of foreach is used where forall could have been used.