Cobra Forums

Posted: **Sun Dec 14, 2008 7:09 am**

The following code does not work.

struct Rational

    var __num as int
    var __den as int
    
    cue init(n as int, d as int)                           #[line 6]
        __num, __den = 0, 1
    
    invariant
        __den <> 0

I get the error (translated from Spanish): "use of possibly unassigned field __den in line 6".

This makes no sense to me, I'm not referring to __den at that line. I tried to inspect the intermediate .cs file but I cannot see the source of the problem.

Maybe invariants cannot be used in structs, but then the error message should be more informative. Besides, if I remove the constructor, the code seems to compile fine. But then I have no way to set the initialize the __den field, so the invariant exception will be thrown as soon as I try to do something with the object:

struct Rational

    var __num as int
    var __den as int
    
    invariant
        __den <> 0
        
    def toString as String is override
        return '[__num]/[__den]'
    
    def main is shared
        r = Rational()
        print r      # Invariant exception!!

Regards,
Manuel

Posted: **Sun Dec 14, 2008 10:49 am**

It's an error from the C# compiler. You can look at the code in foo.cobra.cs which is left in place when a C# error occurs. Be sure to read every line of code that follows a "#line 6".

It's really a false error on C#'s part. The code it is complaining about is guarded by a bool that is set to true at the end of a try { ... } catch, which means __den will be initialized when that code executes, but C# does not do that deep of an analysis.

Regarding a long term fix, I'm not sure. We could have Cobra set all the fields of the struct to something first, but this breaks down if a struct member is a reference to a class that does not have a parameterless constructor. We could try to find some different boilerplate code for checking invariants. If you work on such a solution, just be sure that it does not break anything in Tests\340-contracts.

For now you can work around this by changing the "struct" to a "class", which you probably already guessed.

Posted: **Sun Dec 14, 2008 11:18 am**

Chuck wrote:Be sure to read every line of code that follows a "#line 6".

I didn't suspect there were more lines labelled '6' after line 8

Chuck wrote:If you work on such a solution, just be sure that it does not break anything in Tests\340-contracts.

Don't know, I'll see if I can think of something. Am I wrong to assume that this problem would not exit if the invariant had not been inlined (because then the c# compiler would only see a call to a method, not a direct use of __den)? Maybe inlined invariants are evil, my previous problem also was caused by them.

Posted: **Sun Dec 14, 2008 11:25 am**

No, I tried breaking it out into a method and then C# complains that you cannot access members of "this" until all the fields are initialized (which they are, but it's not smart enough to tell--at least not in .NET 2.0).

Cobra Forums

problem with invariant + struct

problem with invariant + struct

Re: problem with invariant + struct

Re: problem with invariant + struct

Re: problem with invariant + struct