c# - Code Contracts - ForAll - What is supported by static verification -

-

there numerous information static checking of contract.forall has limited or no support.

i did lot of experimenting , found it can work with:

  • contract.forall(items, => != null)
  • contract.forall(items, p) p of type predicate<t>

it cannot work with:

  • field access
  • property access
  • method group (i think delegate allocated here anyway)
  • instance method call

my questions are:

  • what other types of code forall can work with?
  • does code contracts undertand after contract.forall(items, => != null) proven, when taking 1 item list later in code (i.e. indexing), item not null?

here full test code:

public sealed class test {     public bool field;     public static predicate<test> predicate;      [pure]     public bool property     {         { 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, => != null));         contract.assert(contract.forall(items, => != 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.field));         contract.assert(contract.forall(items, => i.field)); // assert unproven     }      public static void test4()     {         var items = new list<test>();         contract.assume(contract.forall(items, => i.property));         contract.assert(contract.forall(items, => 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.instancemethod()));         contract.assert(contract.forall(items, => i.instancemethod()));// assert unproven     } }

i not able find more working expressions, in fact found contract.forall(items, => != null) not working reliably (but understands item not null when later used inside foreach in same function). finally, gave on possibility use more complex forall contracts static checker.

instead devised way control contract static checker, , runtime checker. present method here, in hope might useful people interesting in original question. benefit ability write more complex contracts, can checked @ runtime only, , leave provable contracts static checker (and keep warnings @ low count).

for that, 2 builds debug needed (if don't have them), debug , debug + static contracts, debug build has conditional compilation symbol myproject_contracts_runtime defined. in way receives contract. , rtcontract. contracts. other builds receive contract. contracts.

public static class rtcontract {     [pure] [contractabbreviator] [conditional("myproject_contracts_runtime")]     public static void requires(bool condition)     {         contract.requires(condition);     }      [pure] [contractabbreviator] [conditional("myproject_contracts_runtime")]     public static void ensures(bool condition)     {         contract.ensures(condition);     }      [pure] [conditional("myproject_contracts_runtime")]     public static void assume(bool condition)     {         contract.assume(condition);     } }  public class usage {    void test (int x)    {         contract.requires(x >= 0);  // static , runtime         rtcontract.requires(x.isfibonacci());  // runtime    } }

Comments

Post a Comment

Popular posts from this blog

Java 3D LWJGL collision -

-
i making 3d java game lwjgl library, , wondering how add collision detection, player not go through models. i using obj models. here objloader class, loads models: package renderengine; import java.io.bufferedreader; import java.io.file; import java.io.filenotfoundexception; import java.io.filereader; import java.util.arraylist; import java.util.list; import models.rawmodel; import org.lwjgl.util.vector.vector2f; import org.lwjgl.util.vector.vector3f; public class objloader { public static rawmodel loadobjmodel(string filename, loader loader){ filereader fr = null; try { fr = new filereader(new file("res/"+filename+".obj")); } catch (filenotfoundexception e) { system.err.println("couldn't load file!"); e.printstacktrace(); } bufferedreader reader = new bufferedreader(fr); string line; list<vector3f> vertices = new arraylist<vector3f...
Read more

spring - SubProtocolWebSocketHandler - No handlers -

-
i have ugly error during deploying spring app on jboss. 18:11:16,025 error [org.apache.catalina.core.containerbase.[jboss.web].[default-host].[/consumer]] (msc service thread 1-7) exception sending context initialized event listener instance of class org.springframework.web.context.contextloaderlistener: org.springframework.context.applicationcontextexception: failed start bean 'subprotocolwebsockethandler'; nested exception java.lang.illegalargumentexception: no handlers @ org.springframework.context.support.defaultlifecycleprocessor.dostart(defaultlifecycleprocessor.java:176) [spring-context-4.1.3.release.jar:4.1.3.release] @ org.springframework.context.support.defaultlifecycleprocessor.access$200(defaultlifecycleprocessor.java:51) [spring-context-4.1.3.release.jar:4.1.3.release] @ org.springframework.context.support.defaultlifecycleprocessor$lifecyclegroup.start(defaultlifecycleprocessor.java:346) [spring-context-4.1.3.release.jar:4.1.3.release] @ org.s...
Read more

methods - python can't use function in submodule -

-
my folder structure this: pythonstuff/ program.py modulea/ __init__.py foo.py bar.py here's code bar.py : def hello(): print("hello, world!") here's code program.py : #!/usr/bin/env python3 modulea import bar bar.hello() i run $ python3 program.py somehow error: file "program.py", line 3, in <module> bar.hello() attributeerror: 'module' object has no attribute 'hello' edit: __init__.py file empty. edit2: after trying realized had bar.py in root directory contained hello() method. bar.py in modulea/ directory empty. add it import os __all__ = [] module in os.listdir(os.path.dirname(__file__)): if module != '__init__.py' , module[-3:] == '.py': __all__.append(module[:-3]) the init .py files required make python treat directories containing packages; done prevent directories common name, such string, unintentionally hiding v...
Read more