Code Contracts - ForAll - Was wird durch statische Verifizierung unterstützt

Question

Es gibt zahlreiche Informationen, die statische Überprüfung von Contract.ForAll hat nur begrenzte oder keine Unterstützung.

Ich habe viel experimentiert und fand kann es mit arbeiten:

• Contract.ForAll(items, i => i != null)
• Contract.ForAll(items, p) wo p vom Typ Predicate<T>

es kann nicht Arbeit mit:

• Feld Zugang
• Zugang zur Immobilie
• Methodengruppe (ich glaube, delegieren hier sowieso zugeordnet ist)
• Instanz Methodenaufruf

Meine Fragen sind:

• Was sind andere Arten von Code, mit denen ForAll arbeiten kann?
• Entspricht der Code Contracts, dass nach Contract.ForAll(items, i => i != null) bewiesen ist, dass wenn ein Element aus der Liste später im Code (d. H. Durch Indizierung) genommen wird, das Element nicht null ist?

ist hier voll Testcode:

public sealed class Test 
{ 
    public bool Field; 
    public static Predicate<Test> Predicate; 

    [Pure] 
    public bool Property 
    { 
     get { return Field; } 
    }  

    [Pure] 
    public static bool Method(Test t) 
    { 
     return t.Field; 
    } 

    [Pure] 
    public bool InstanceMethod() 
    { 
     return Field; 
    } 

    public static void Test1() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i != null)); 
     Contract.Assert(Contract.ForAll(items, i => i != null)); // OK 
    } 

    public static void Test2() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, Predicate)); 
     Contract.Assert(Contract.ForAll(items, Predicate)); // OK 
    } 

    public static void Test3() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i.Field)); 
     Contract.Assert(Contract.ForAll(items, i => i.Field)); // assert unproven 
    } 

    public static void Test4() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i.Property)); 
     Contract.Assert(Contract.ForAll(items, i => i.Property)); // assert unproven 
    } 

    public static void Test5() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, Method)); 
     Contract.Assert(Contract.ForAll(items, Method)); // assert unproven 
    } 

    public static void Test6() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i.InstanceMethod())); 
     Contract.Assert(Contract.ForAll(items, i => i.InstanceMethod()));// assert unproven 
    } 
} 

Answer 1

von decompiling mscorelib.dll System.Diagnostics.Contracts wir sehen easely können, wie Contract.ForAll gebaut: Es dauert Sammlung und Prädikat.

public static bool ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate) 
{ 
    if (collection == null) 
    { 
     throw new ArgumentNullException("collection"); 
    } 
    if (predicate == null) 
    { 
     throw new ArgumentNullException("predicate"); 
    } 
    foreach (T current in collection) 
    { 
     if (!predicate(current)) 
     { 
      return false; 
     } 
    } 
    return true; 
} 

Also, wenn Sie Contract.ForAll(items, i => i.Field) in diesem Fall sagen i => i.Field ist Prädikat

dann von Ihrem Beispiel in allen Testverfahren folgen, können wir sehen, dass Sie eine leere Liste zu Contract.ForAll Verfahren bereitzustellen, die als es wahr zurück wird niemals in den foreach-Block eintreten.

es weiter machen, wenn Sie Artikel auf Ihrer Liste var items = new List<Test>() {new Test()}; hinzufügen und führen Sie den Test erneut als public bool Field; return false wird standardmäßig

Das Ziel Contract.ForAll ist

falsch ist

Bestimmt, ob alle Elemente in einer Sammlung existieren innerhalb einer Funktion

Also meine Schlussfolgerung ist, dass es sich nicht um C Ontart.ForAll kann nicht mit etwas arbeiten, es ist eher mindestens ein Element in Ihrer Sammlung gibt false zurück oder ist null

Answer 2

Ich konnte nicht mehr funktionierende Ausdrücke finden, in der Tat fand ich, dass auch Contract.ForAll(items, i => i != null) nicht zuverlässig funktioniert (aber Es versteht, dass das Element nicht null ist, wenn es später innerhalb von foreach in derselben Funktion verwendet wird. Schließlich gab ich die Möglichkeit auf, komplexere ForAll-Verträge mit statischen Checkern zu verwenden.

Stattdessen habe ich eine Möglichkeit entwickelt, um zu steuern, welchen Vertrag für statische Checker und welche für Laufzeit-Checker sind. Ich stelle diese Methode hier vor, in der Hoffnung, dass es für Leute nützlich sein könnte, die in der ursprünglichen Frage interessant sind. Der Vorteil ist die Fähigkeit, komplexere Verträge zu schreiben, die nur zur Laufzeit überprüft werden können und nur leicht beweisbare Verträge für statische Prüfer hinterlassen (und die Warnungen einfach auf niedriger Zahl halten).

Dafür 2 baut Debug benötigt werden (wenn Sie nicht bereits haben), Debug und Debug + Static Verträge, The Debug build bedingte Kompilierung Symbol MYPROJECT_CONTRACTS_RUNTIME definiert hat. Auf diese Weise erhält es alle Contract. und RtContract. Verträge. Andere Builds erhalten nur Contract. Verträge.