ensure no changes to method parameters

Question

Hello, how can I make contract ensuring no changes to non primitive parameters?

What i want to prove about my code is that program counter is in bounds of the program in each step. I have some initial value and set of labels for whose addresses i need to prove (or at least assume) that their addresses are also within bounds and then any execution of any instruction (declaration,increment,decrement,conditional jump) keeps program counter in bounds. I believe that most of "ensures unproven" are caused by the inability to state that set of labels does not change in places where i want to prove that 'pc = labels[label]' does not move pc out of bounds. I am also frustrated that

private List<Instruction> program = new List<Instruction>();
private Dictionary<string, int> labels = new Dictionary<string, int>();

private void test ()
{

  Contract.Ensures(Contract.ForAll(labels.Keys, label => labels[label] < program.Count));
  Contract.Assume(Contract.ForAll(labels.Keys, label => labels[label] < program.Count));

  //pc = program[pc].execute(pc, labels, vars);//Here i need to specify that Dictionary<string, int> labels is not modified by Instruction.execute
}

would not lead to proving the "ensures" even when i dont add the call that is commented out.

Could anyone, please, provide me an example of how to ensure that a method parameter is not changed in a particular method?

EDIT:

example for what I cannot overcome:

// There are no invalid labels just yet
Contract.Assume(Contract.ForAll(labels.Keys, label => labels[label] < program.Count));

if (i is InstructionLabel)
{
  string label = ((InstructionLabel)i).label;
  labels[label] = program.Count - 1;
  Contract.Assume(labels[label] < program.Count);
}

Contract.Assert(Contract.ForAll(labels.Keys, label => labels[label] < program.Count));

this leads to: CodeContracts: assert unproven

Answer 1

Hi,

Your usage of ForAll is too complex for the static checker.

From the Contracts User Manual, §6.6.1:

"The static contract checker has limited supported for ForAll quantifiers, provided the quantified expression is simple like x => x != null."

However, in my experience even simple quantifiers like x => x != null are often unproven.

You can solve this problem by expanding quantifiers into discrete methods to avoid static checker warnings while retaining full runtime support.  The following example has no warnings.

(In the future, please post short but complete programs that can reproduce your problem.)

using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;

namespace CCTest
{
	class ComplexForAll
	{
		private readonly Dictionary<string, int> labels = new Dictionary<string, int>();
		private readonly List<Instruction> program;

		public ComplexForAll(IEnumerable<Instruction> program)
		{
			Contract.Requires(program != null);
			Contract.Requires(Contract.ForAll(program, instruction => instruction != null));

			this.program = new List<Instruction>(program);

			Contract.Assert(AllInstructionsAreNotNull());
			Contract.Assert(AllLabelsAreLessThanProgramCount());
		}

		[ContractInvariantMethod]
		[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Performance", "CA1822:MarkMembersAsStatic", Justification = "Required for code contracts.")]
		private void ObjectInvariant()
		{
			Contract.Invariant(labels != null);
			Contract.Invariant(program != null);
			Contract.Invariant(AllInstructionsAreNotNull());
			Contract.Invariant(AllLabelsAreLessThanProgramCount());
		}

		[Pure, ContractVerification(false)]
		private bool AllInstructionsAreNotNull()
		{
			Contract.Ensures(Contract.Result<bool>() == program.All(instruction => instruction != null));

			return program.All(instruction => instruction != null);
		}

		[Pure, ContractVerification(false)]
		private bool AllLabelsAreLessThanProgramCount()
		{
			Contract.Ensures(Contract.Result<bool>() == labels.All(pair => labels[pair.Key] < program.Count));

			return labels.All(label => labels[label.Key] < program.Count);
		}

		public void SetLabel(Instruction i)
		{
			var label = i as InstructionLabel;

			if (label != null)
			{
				labels[label.Label] = program.Count - 1;
			}
		}

		private void Execute(params object[] vars)
		{
			for (int i = 0; i < program.Count; i++)
			{
				var current = program[i];

				Contract.Assume(current != null);

				current.Execute(i, labels, vars);
			}

			Contract.Assert(AllLabelsAreLessThanProgramCount());
		}

		public abstract class Instruction
		{
			public abstract void Execute(int number, IDictionary<string, int> labels, params object[] vars);
		}

		public class InstructionLabel : Instruction
		{
			public string Label { get; set; }

			public override void Execute(int number, IDictionary<string, int> labels, params object[] vars)
			{
			}
		}
	}
}

- Dave

---

http://davesexton.com/blog

Answer 2

Thank you! I need static checks but there is probably no way of getting it work now. Any idea about the other Ensures? ("Parameter not modified")

Answer 3

Hi,

> I need static checks but there is probably no way of getting it work now.

It's not entirely lost.  Note that I'm using Assert in my example, not Assume.  Assert is analyzed by the static checker.

> Any idea about the other Ensures? ("Parameter not modified")

Actually, I may have uncovered a bug in the static checker.  The Execute method in my example calls the following after the loop:

Contract.Assert(AllLabelsAreLessThanProgramCount());

Note that I'm calling Assert, which means that the static checker must verify the contract, yet there are no warnings.

It would seem that this is a false negative, because the example calls the following inside the loop:

current.Execute(i, labels, vars);

The Instruction.Execute method has no contracts indicating that labels will be unmodified; therefore, I would expect the static checker to warn that the assertion is unproven, since it depends on labels.

In other words, the example asserts that AllLabelsAreLessThanProgramCount is true.  It returns true only if labels hasn't been modified by Instruction.Execute, which of course cannot be proven.

I wonder if this is a bug or simply a known limitation of the static checker.

Regardless, you can specify the following contracts to indicate that Instruction.Execute doesn't modify the labels parameter; however, notice the complexity of the quantifiers are still too great for the static checker to prove them, so you're back to the beginning again.

[ContractClass(typeof(InstructionContract))]
public abstract class Instruction
{
	public abstract void Execute(int number, IDictionary<string, int> labels, params object[] vars);
}

[ContractClassFor(typeof(Instruction))]
internal abstract class InstructionContract : Instruction
{
	public override void Execute(int number, IDictionary<string, int> labels, params object[] vars)
	{
		Contract.Requires(labels != null);
		Contract.Ensures(Contract.OldValue(labels).Count == labels.Count);
		Contract.Ensures(Contract.Exists(labels.Keys, label => Contract.OldValue(labels).ContainsKey(label)));
		Contract.Ensures(Contract.ForAll(labels.Keys, label => Contract.OldValue(labels)[label] == labels[label]));
	}
}

Therefore, it's probably best to constrain the type as a read-only dictionary.  Using the type system is often the best way to define and enforce contracts.  And in this case, Dictionary<TKey, TValue> implements IReadOnlyDictionary<TKey, TValue>, so you get it for free!

[ContractClass(typeof(InstructionContract))]
public abstract class Instruction
{
	public abstract void Execute(int number, IReadOnlyDictionary<string, int> labels, params object[] vars);
}

[ContractClassFor(typeof(Instruction))]
internal abstract class InstructionContract : Instruction
{
	public override void Execute(int number, IReadOnlyDictionary<string, int> labels, params object[] vars)
	{
		Contract.Requires(labels != null);
	}
}

Alternatively, you can simply make an assumption at the callsite:

current.Execute(i, labels, vars);
Contract.Assume(AllLabelsAreLessThanProgramCount());

- Dave

---

http://davesexton.com/blog

Answer 4

A little and probably stupid question: program.All and labels.All are not defined functions over here ... program.TrueForAll seems to be as good as All but for labels there is no such thing :/... am i doing something wrong?

Answer 5

Hi,

Did you forget to add this?

using System.Linq;

- Dave

---

http://davesexton.com/blog

Answer 6

I noticed it so i tried to remove my post but it did not get deleted, sorry about that.

I continue to have problems :/ Now it boils down to:

using System;
using System.Collections.Generic;
using System.IO;
using System.Text;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using System.Diagnostics.Contracts;

namespace Interpreter
{
public void A(List<String> a)
{
  a.Add("Hi");
  throw new Exception(Contract.OldValue(a.Count).ToString() + " " + a.Count.ToString());
}

[TestMethod]
public void B()
{
  List<String> a = new List<String>(new String[] {"Hello"});
  a.Add("Hey");
  A(a);
}
}

public void A(List<String> a)
{
  a.Add("Hi");
  throw new Exception(Contract.OldValue(a).Count.ToString() + " " + a.Count.ToString());
}

[TestMethod]
public void B()
{
  List<String> a = new List<String>(new String[] {"Hello"});
  a.Add("Hey");
  A(a);
}

1) throws an exception with message "0 3" while i expect "2 3".

2) null pointer exception

Is this caused by my stupidity / bug / some kind of optimizations (inlinement of the tested method A)?

Answer 7

OK problem was in VS2012 and its new handling of exceptions thrown during tests. I needed to use Legacy mode by providing legacy.runsettings file with ForceLegacyMode:

<?xml version="1.0" encoding="utf-8" ?>
<RunSettings>
  <MSTest>
    <ForcedLegacyMode>true</ForcedLegacyMode>
  </MSTest>
</RunSettings>

and add it as test settings throw: Test -> Test Settings ...

And then using:

public sealed class ExpectedContractViolationAttribute : ExpectedExceptionBaseAttribute
        {
            const string ContractExceptionName = "System.Diagnostics.Contracts.__ContractsRuntime+ContractException";
            string msg;

            public ExpectedContractViolationAttribute(string msg)
            {
                this.msg = msg;
            }

            protected override void Verify(Exception exception)
            {
                if (exception.GetType().FullName.Equals(ContractExceptionName))
                {
                    if (!exception.Message.Equals(msg))
                    {
                        throw new Exception("\"" + exception.Message + "\" != \"" + msg + "\"");
                    }
                }
                else
                {
                    throw exception;
                }
            }
        }