Invariants on interface properties?

hey guys,

it's me again. today tried define contracts on interfaces. thus, it's working methods, got problems on properties, i've defined on interface.

let's consider interface/contract-class pair:

1	[contractclass(typeof(contractforiaccount))]
2	public interface iaccount
3	{
4	float balance { get; }
5
6	bool withdraw(float amount);
7	void deposit(float amount);
8	}
9
10	[contractclassfor(typeof(iaccount))]
11	class contractforiaccount : iaccount
12	{
13	[contractinvariantmethod]
14	protected void objectinvariant()
15	{
16	contract.invariant(((iaccount)this).balance >= 0);
17	}
18
19	float iaccount.balance
20	{
21	get
22	{
23	return default(float);
24	}
25	}
26
27	bool iaccount.withdraw(float amount)
28	{
29	contract.requires(amount > 0);
30
31	return default(bool);
32	}
33
34	void iaccount.deposit(float amount)
35	{
36	contract.requires(amount > 0);
37	}
38	}

here defined object invariant in contract class interface. now, if let class implement interface, static checker doesn't seem know object invariant. can have private setter on "balance" , say: "balance = -1" , works (static checker doesn't warn), should not allowed due invariant...

any suggestions/comments on that?


thanks, matthias

hi matthias,

object invariants not supported on interfaces @ moment. can see why might handy though.

at moment need specify property invariants writing pre-condition on setter , post condition on getter (or on getter if don't have setter).

so in case, become:

float iaccount.balance

{

get

{

contract.ensures(contract.result<float>() >= 0.0);

return default(float);

}

}

now, force implementation of getter prove non-negative. how can getter non-negative time. well, have add invariant on backing field balance implementation.

thus, writing ensures on getter, may force implementor have invariants indirectly.

---

cheers, -maf (manuel fahndrich)

DevLabs  >  Code Contracts