Hello,

I'm developing a project in Spec# and I got the warning:

Warning 1 method invocation may violate the modifies clause of the enclosing method 

I have this class structure:

public bool createNewTask(TeamDevelop teamDevelop, string description, int startingDate, int endDate)
			
			requires startingDate<=endDate;
		{
			bool result = false;

			if(this.isManager()){
				if(datesAreValid(teamDevelop.project,startingDate,endDate)){
					if(checkTeamDevelopAvailability(teamDevelop)){
					
							Task t = new Task(teamDevelop,description,startingDate,endDate);
							teamDevelop.tasks.Add(t);
							result  = true;
						
				}
			} 
			}
			return result;
		}

And in the class Task I have:

public class Task {

		...
        [Peer] public TeamDevelop developer;
		
	invariant this.startingDate <= this.endDate;

        public Task([Captured]TeamDevelop t ,string desc , int sdate , int edate)
			requires sdate <= edate;
        {
			assert sdate<= edate;

			this.description = desc;
			this.startingDate = sdate;
			this.endDate = edate;
			this.developer = t;
			this.isClose = false;
			this.isOpen = false;
			this.isWaitingForAcceptance = false;
        }

The warning is on the underlined line. What can I be doing wrong to get that error?

Best Regards,

mbalves

I suspect it's because Task captures t, which means it will change the owner of t.  But the caller does not have the right to change the caller of teamDevelop.  I didn't try it, but I'm guessing the error will go away if you mark createNewTask's teamDevelop with [Captured] as well.

  Rustan

Thanks for the reply. I tried to mark teamDevelop with Captured and the warning is now on :

teamDevelop.tasks.Add(t);

I got now two warning in that line.

- Call of System.Collections.Generic.ICollection<Task!>.Add(Task! item), unsatisfied precondition: !this.IsReadOnly

- method invocation may violate the modifies clause of the enclosing method 

I think these warnings are just what you'd expect.

The first warning simply means that it is not known whether or not teamDevelop.tasks is readonly (and you're not allowed to invoke Add on a readonly collection).  I don't know how you would like to ensure that teamDevelop.tasks is not readonly.  One possibility would be to add it as a precondition of createNewTask, but it may be better to try to add something to the object invariant of TeamDevelop.

The second warning simply means that the effect of Add is not allowed in createNewTask.  One possible way to resolve this is to add teamDevelop.tasks to the modifies clause of createNewTask (I'm assuming "tasks" is probably declared with [Peer]).

For your application, I can't determine if the suggestions I made here are the design decisions you want, so you may need to give it some thought or experiment a bit until you figure out what design you want.

By the way, the Task constructor puts the "t" parameter into the "developer" field, which is declared with [Peer].  An alternative to declaring "t" with [Captured], you may want to consider declaring the Task being constructed as [Captured].  I think (hope) there is a section in the Spec# Tutorial that explains how to do this and the pros and cons.

  Rustan