Questo è un bug nel correttore contratto di statica?

Question

Se scrivo questo:

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        if (count == 1)
            owner = null;
        --count;
    }
}

Il correttore contratto statica può dimostrare tutte le asserzioni.

Ma se scrivo questo, invece:

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        --count;
        if (count == 0)
            owner = null;
    }
}

Si rivendica il owner == null || count > 0 postcondizione non è provata.

Credo di poter dimostrare la seconda forma non viola questa postcondizione:

// { count > 0 } it's required
--count;
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero
if (count == 0)
{
    // { count == 0 } the if condition is true
    owner = null;
    // { count == 0 && owner == null } assignment works
}
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not
// { owner == null || count > 0 } we can assume a weaker postcondition

E 'qualcosa di sbagliato con la mia prova?

ho aggiunto le affermazioni nella mia prova come le chiamate Contract.Assert al codice, e sono arrivato alla conclusione che se aggiungo solo questo, riesce a dimostrare la postcondizione:

--count;
Contract.Assert(count == 0 || count > 0)
if (count == 0)
    owner = null;

Ma, se ora posso cambiare la stessa asserzione ad un modo "più naturale", non riesce:

--count;
Contract.Assert(count >= 0)
if (count == 0)
    owner = null;

Ci si aspetterebbe che queste due asserzioni erano equivalenti, ma il correttore statica li tratta diversamente.

(sto usando la beta 2 del VS10 tra l'altro)

Answer 1

Non mi aspettavo questa cosa molto complessa prover ad essere in uno stato completamente funzionante ma dal momento che è solo una versione beta, dopo tutto. Penso che sia un bug o almeno un punto degno di sollevare con gli sviluppatori, perché questa è una cosa molto semplice da verifica statica automaticamente.

In ogni caso, tramite gli sguardi delle cose, il marcatore assicura è solo lì per dire se il correttore contratto di statica è in grado di garantire la condizione o meno. Questo non implica che la condizione non è valida, significa solo non riesce a trovare una prova.

Sarei molto più preoccupato per i casi in cui si dice qualcosa è assicurato che non è valido. che conterebbe come un bug!

Answer 2

Caveat: So assolutamente nulla sulle specifiche del sistema contrattuale .net

.

Tuttavia, posso dirvi questo: è letteralmente non è possibile (cfr problema della terminazione) per produrre una cella completa per affermazioni ricco come quello che appare questo sistema supporta.

Quindi: è questo un bug? N

D'altra parte, sembra plausibile suggerire che questo potrebbe essere un caso comune che gli implementatori della cella potrebbe desiderare di aggiungere al loro sistema.