Quão livre posso estar no código em um objeto invariante?

Question

Estou tentando demonstrar invariantes em contratos de código e pensei em dar um exemplo de uma lista classificada de strings. Ele mantém uma matriz internamente, com espaço sobressalente para adições etc. - assim como List<T>, basicamente. Quando precisa adicionar um item, ele o insere na matriz, etc. Achei que tinha três invariantes:

• A contagem deve ser sensata: não negativa e no máximo o tamanho do buffer
• Tudo na parte não utilizada do buffer deve ser nula
• Cada item na parte usada do buffer deve ser pelo menos tão "grande" quanto o item antes dele

Agora, tentei implementar isso desta maneira:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(count >= 0 && count <= buffer.Length);
    for (int i = count; i < buffer.Length; i++)
    {
        Contract.Invariant(buffer[i] == null);
    }
    for (int i = 1; i < count; i++)
    {
        Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0);
    }
}

Infelizmente, ccrewrite está bagunçando os loops.

A documentação do usuário diz que o método deve ser apenas uma série de chamadas para Contract.Invariant. Eu realmente tenho que reescrever o código como algo assim?

Contract.Invariant(count >= 0 && count <= buffer.Length);
Contract.Invariant(Contract.ForAll
    (count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll
    (1, count, i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

Isso é um pouco feio, embora funcione. (É muito melhor do que minha tentativa anterior, lembre -se.)

Minhas expectativas são irracionais? Meus invariantes são irracionais?

(Também perguntado como um Pergunta no fórum de contratos de código. Vou adicionar respostas relevantes aqui.)

Answer 1

A partir das páginas (preliminares) do MSDN, parece que o contrato. Para todos os membros, pode ajudá -lo com os 2 contratos de intervalo. A documentação não é muito explícita sobre sua função.

//untested
Contract.Invariant(Contract.ForAll(count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll(1, count, 
    i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

Answer 2

(Vou aceitar a resposta de Henk, mas acho que vale a pena acrescentar isso.)

A pergunta já foi respondida no Fórum MSDN, e o resultado é que a primeira forma não é espera -se funcionar. Invariantes realmente precisam ser uma série de chamadas para Contract.Invariant, e isso é tudo.

Isso torna mais viável para o verificador estático entender o invariante e aplicá -lo.

Essa restrição pode ser contornada simplesmente colocando toda a lógica em um membro diferente, por exemplo, um IsValid propriedade, e depois chamando:

Contract.Invariant(IsValid);

Isso, sem dúvida, atrapalharia o verificador estático, mas em alguns casos pode ser uma alternativa útil em alguns casos.

Answer 3

Os designers não estão reinventando a roda um pouco?

O que havia de errado com o bom velho

bool Invariant() const; // in C++, mimicking Eiffel

?

Agora, em C#, não temos const, mas por que você não pode simplesmente definir um Invariant função

private bool Invariant()
{
  // All the logic, function returns true if object is valid i.e. function
  // simply will never return false, in the absence of a bug
}
// Good old invariant in C#, no special attributes, just a function

E então basta usar os contratos de código em termos dessa função?

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(Invariant() == true);
}

Talvez eu esteja escrevendo bobagens, mas mesmo nesse caso, ele terá algum valor didático quando todos me disserem errado.