Soundness

• dafny

  31 2,665 9.7 C#

  Dafny is a verification-aware programming language

  

As you can see it is fully functional and only creates a finite (and small) number of objects. This code is public, since it was posted to the Dafny bug tracker I'm currently writing some articles about it. trait BadTrait{function method contradiction():()ensures false}   class BadClass{ const tr: BadTrait   constructor(tr: BadTrait) { this.tr := tr; }   } class T { const f: T -> BadClass   constructor(f: T -> BadClass) { this.f := f; }   } function method app(x: T): BadClass {  x.f(x) } method Main() { var x := new T(app);   ghost var \_ := app(x).tr.contradiction();   assert false;   print "false is true!"; // actually prints! } As you can see, Ghost+termination_bug = soundness_bug

• InfluxDB

  www.influxdata.com sponsored

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

Suggest a related project