Rep and Additive

Wiki Link: [discussion:281548]
afazeli
Dec 1, 2011 at 11:16 PM

Hi,

I tried to make a Rep field Additive to use it in one of the invariants of an inherited class, but the compiler didn't not allow it. Then I tried to do it by get property, compiler complains that this is not a Rep field. Actually I have two synonym invariants, I tried them both and following are the invariants and their corresponding error messages.

 

invariant exists {int i in (0: numRunways); Runways[i].IntRunway};

 

Error 20 Expression is not admissible: it is not visibility-based, and first access 'get_Runways' is non-rep thus further field access is not admitted. C:\Users\Adnan\documents\visual studio 2010\Projects\SpecSharp2010\SpecSharp2010\Airports\InternationalAirport.ssc 11 47 SpecSharp2010

invariant exists {Runway! r in Runways; r.IntRunway};

Error 20 Expression is not admissible: first access on array or binding member must be rep. C:\Users\Adnan\documents\visual studio 2010\Projects\SpecSharp2010\SpecSharp2010\Airports\InternationalAirport.ssc 12 34 SpecSharp2010

Is there a way to use a Rep field of a base class in the invariants of an inherited class.

Thanks,

Adnan
mueller
Developer
Dec 2, 2011 at 7:17 AM

Hi Adnan,

What you are trying to do should work. As I said before, it would help us a lot if you could provide us with a small (!) repro of your error.

  Peter
afazeli
Dec 8, 2011 at 8:03 PM
Edited Dec 8, 2011 at 8:04 PM

Hi,

The following is a small repro of the probelm, there are other verification warnings like "Warning 12 Cannot prove that Method .ctor does not write global variables C:\Users\Adnan\documents\visual studio 2010\Projects\Test\Test\Main\AdditiveAndRep.ssc 71 10 Test" and others which I hope you can help to solve them, It is not clear what is the reason for these warnings.

 

using System;
using System.Collections.Generic;
using Microsoft.Contracts;

namespace Main{

	public class Airport
    {

        [SpecPublic] private string code;
        [Additive] protected int numRunways;
        [SpecPublic][Rep][ElementsRep] protected List<Runway!>! runways = new List<Runway!>();
        
		invariant numRunways >= 1 && numRunways <= 30;
		invariant runways.Count == numRunways;
		      
	[NotDelayed]
        public Airport(String? code, int numRunways )
        requires exists unique {string! aCode in ValidCodes.airportCodes; aCode == code};
        requires numRunways >= 1 && numRunways <= 30;
        {
			this.code = code;
			this.numRunways = numRunways;
			for(int i = 0; i<numRunways; i++)
			{
				Runway! r = new Runway();
				runways.Add(r);	
			}
        }
		
		 public string Code
        {

            get { return code; }
            set modifies this.code;
				requires value != null; 
				requires exists unique{string aCode in ValidCodes.airportCodes; value == aCode };
				{ code = value; }
        } 
		
		public List<Runway!>! Runways{
			get { return runways;}
			
			[Additive] set 
			//requires Owner.None((List<Runway!>!)value);
			//requires forall{Runway r in value; Owner.None(r)};
			requires value != null;
			modifies runways, numRunways;
			ensures runways == value;
			{ 
				additive expose(this){
					runways = value;
					numRunways = value.Count;
				}	
			}
		}
		
    }

	public class InternationalAirport: Airport{
	
		invariant numRunways >= 10;
		//invariant exists {int i in (0: numRunways); Runways[i].IntRunway};
		invariant exists {Runway! r in Runways; r.IntRunway};
		
		[NotDelayed]
		public InternationalAirport(string code): base(code, 10){}
		
		
		[NotDelayed]
		public InternationalAirport(string code, int numRunways): base(code, numRunways)
		requires numRunways >= 10;
		//ensures exists {int i in (0: numRunways); runways[i].IntRunway}; 
		ensures exists {Runway! runway in runways; runway.IntRunway};
		{} 
	}

	public class Runway
	{
        protected int length;
        protected int width;

		[SpecPublic] model bool IntRunway {
			satisfies IntRunway == (length >= 80 && width >= 10);
		}
		
		invariant length >= 40 && length <= 100;
		invariant width >= 5 && width <= 15;


        [NotDelayed]
		public Runway()
        {
			this.length = 70;
            this.width = 5;
        }

        public int Length
        {
			
			get { return length; }
            set 
            requires value >= 40 && value <= 100;
			requires IntRunway ==> value >=80;
            modifies length;
            ensures length == value;
			ensures IntRunway ==> length >=10;
			{ 
				length = value; 
			}
        }


        public int Width
        {

            get { return width; }
            set 
            requires value >= 5 && value <= 15;
			requires IntRunway ==> value >=10;
            modifies width;
            ensures width == value;
			ensures IntRunway ==> width >=10;
            { 
				width = value; 
			}
        }
	}

	public class ValidCodes 
	{
		[Rep] public static HashSet<string> airportCodes = new HashSet<string>{"PWD","NYC","BOS"};
	}
}

 

Thanks,

Adnan
mueller
Developer
Dec 14, 2011 at 8:05 AM

Hi Adnan,

Spec# checks the admissibility of invariants syntactically. Since you are using the property Runways, it does not recognize that you are dereferencing a rep-field. If you use the field runways instead, this error disappears. However, then you get another error that a rep-field must not be additive. I need to explore this futher.

   Peter
Sign in to post message or set email notifications