Examples

Here is a simple B3 program to whet your appetite.

// Here is a little comment

type List
tagger ListTag for List

function Nil(): List tag ListTag
function Cons(injective head: int, injective tail: List): List tag ListTag

function Length(list: List): int
axiom forall list: List pattern Length(list) 0 <= Length(list)

procedure TestLists(list: List) {
  var n := Length(list)
  check n != -9
}

Here is a longer example:

// This example program shows many B3 features in use. The main point is to prove
// that GetPublicAccessBlock is called with a bucket name that satisfies UserOwnsBucket.
// This properties is guaranteed by the postcondition of ListBuckets, which, upon
// success, returns a sequence where every bucket name satisfies GetPublicAccessBlock.
//
// Here is the program shown in the syntax of a Dafny-like programming-language:
//
//     var fileSystem :- CreateClient("myFileSystemName")
//     var aresponse :- fileSystem.ListBuckets()
//     var buckets := aresponse.buckets
//     for i := 0 to |buckets| {
//       var bucket := buckets[i]
//       var bucketName := bucket.name
//       var bresponse :- fileSystem.GetPublicAccessBlock(bucketName)
//       var isBlocked := bresponse.getConfig.GetAttributeValue("BlockPublicAcls")
//       if isBlocked {
//         print "bucket", bucketName, "is blocked"
//       } else {
//         print "bucket", bucketName, "is not blocked"
//       }
//      }
//
// Note that B3 identifiers may contain "." characters. B3 uses ".." as part of the
// name when it generates functions (for example, the function names generated as a result
// of declaring a parameter to be "injective").

procedure Good(out result: XResult) {
  var cresult: CResult
  CreateClient(|myFileSystemName: string|, out cresult)
  if !CIsSuccess(cresult) {
    result := XFailure(CFailure..msg(cresult))
    return
  }
  var fileSystem := CSuccess..value(cresult)

  var aresult: AResult
  ListBuckets(fileSystem, out aresult)
  if !AIsSuccess(aresult) {
    result := XFailure(AFailure..msg(aresult))
    return
  }
  var aresponse := ASuccess..value(aresult)

  var buckets := AResponse..buckets(aresponse)

  var i := 0
  loop
    invariant 0 <= i && i <= length(buckets)
  {
    if i == length(buckets) {
      exit
    }
    
    check 0 <= i && i < length(buckets)
    var bucket := select(buckets, i)

    var bucketName := Bucket..name(bucket)

    var bresult: BResult
    GetPublicAccessBlock(fileSystem, bucketName, out bresult)
    if !BIsSuccess(bresult) {
      result := XFailure(BFailure..msg(bresult))
      return
    }
    var bresponse := BSuccess..value(bresult)
 
    var isBlocked := GetAttributeValue(BResponse..getConfig(bresponse), |BlockPublicAcls: string|)

    if isBlocked {
      Print(|bucket: string|, bucketName, |is-blocked: string|)
    } else {
      Print(|bucket: string|, bucketName, |is-not-blocked: string|)
    }

    i := i + 1
  }

  var x: X
  result := XSuccess(x)
}

// --------------------------------------------------------------------

// The file-system API is the following:

procedure CreateClient(name: string, out result: CResult)

// This predicate says whether or not the given bucket name is owned by the user.
// It is used in the postcondition of ListBuckets and in the precondition of
// GetPublicAccessBlock.
function UserOwnsBucket(name: string): bool

type Client

procedure ListBuckets(c: Client, out aresult: AResult)
  ensures AIsSuccess(aresult) ==>
    forall bucket: Bucket
      pattern Bucket..name(bucket)
      pattern in(bucket, AResponse..buckets(ASuccess..value(aresult)))
      in(bucket, AResponse..buckets(ASuccess..value(aresult))) ==>
      UserOwnsBucket(Bucket..name(bucket))

procedure GetPublicAccessBlock(c: Client, Bucket: string, out result: BResult)
  requires UserOwnsBucket(Bucket)

// --------------------------------------------------------------------

// The example program uses an API model where each API entry point returns a "response".
// This is typical in many code bases, for example in Java, because it allows the API
// to evolve to add more attributes of the response in the future. What that means for
// the example program is that there are different response types. Here, those are modeled
// as records with one just field.

// datatype AResponse = AResponse(buckets: BucketSeq)
type AResponse
function AResponse(injective buckets: BucketSeq): AResponse

// datatype BResponse = BResponse(getConfig: BlockConfig)
type BResponse
function BResponse(injective getConfig: BlockConfig): BResponse

// --------------------------------------------------------------------

// For the purpose of the example, a bucket is something that has a name. In a full API,
// buckets would also have some data, of course.

// datatype Bucket = Bucket(name: string)
type Bucket
function Bucket(injective name: string): Bucket

// --------------------------------------------------------------------

// In the example, a block configuration is a set of named attributes, each of which can
// be false or true.

type BlockConfig

function GetAttributeValue(config: BlockConfig, attribute: string): bool

// --------------------------------------------------------------------

// The example program is written in the style of Rust, Go, and Dafny, where a failure
// is reported as a special return value that have to be tested by the caller. In Go,
// such querying and propagation of failures is done manually, whereas Rust has the
// "?" operator and Dafny has the ":-" operator for doing this. Such code is translated
// into B3 by doing the checking explicitly.
//
// Using datatypes with type parameters, such Result types can be defined as
//
//     datatype Result<X> = Success(value: X) | Failure(msg: string)
//
// Since B3 does not support polymorphism, there is one Result type for each success
// type.

type X
type XResult // Result<()>
tagger XResultTag for XResult
function XSuccess(injective value: X): XResult tag XResultTag
function XFailure(injective msg: string): XResult tag XResultTag
function XIsSuccess(r: XResult): bool {
  XResultTag(r) == XSuccess..tag()
}

type CResult // Result<Client>
tagger CResultTag for CResult
function CSuccess(injective value: Client): CResult tag CResultTag
function CFailure(injective msg: string): CResult tag CResultTag
function CIsSuccess(r: CResult): bool {
  CResultTag(r) == CSuccess..tag()
}

type AResult // Result<AResponse>
tagger AResultTag for AResult
function ASuccess(injective value: AResponse): AResult tag AResultTag
function AFailure(injective msg: string): AResult tag AResultTag
function AIsSuccess(r: AResult): bool {
  AResultTag(r) == ASuccess..tag()
}

type BResult // Result<BResponse>
tagger BResultTag for BResult
function BSuccess(injective value: BResponse): BResult tag BResultTag
function BFailure(injective msg: string): BResult tag BResultTag
function BIsSuccess(r: BResult): bool {
  BResultTag(r) == BSuccess..tag()
}

// --------------------------------------------------------------------

// Finally, we have a type BucketSeq that models a sequence of buckets
// and a(n uninterpreted) string type whose values can be printed.
//
// In a source programming language, the "select" operation on a sequence
// has a precondition that the given index is in range. The example B3 code
// above uses a "check" statement to enforce that precondition.

type BucketSeq

function select(s: BucketSeq, i: int): Bucket

function length(s: BucketSeq): int

axiom explains length
  forall s: BucketSeq
    pattern length(s)
    0 <= length(s)

function in(b: Bucket, s: BucketSeq): bool {
  exists i: int
    pattern select(s, i)
    0 <= i && i < length(s) && select(s, i) == b
}

type string

procedure Print(a: string, b: string, c: string)

Here are examples that show union types and discriminated union types:

type X
type Y

// Union is like a C type
//     union {
//       X x;
//       Y y;
//     }

type Union
function XUnion(injective getX: X): Union
function YUnion(injective getY: Y): Union

procedure TestUnion(x: X, y0: Y, y1: Y)
{
  var ux := XUnion(x)
  var uy0 := YUnion(y0)
  var uy1 := YUnion(y1)

  check ux != uy0 // error: this is not provable
  check y0 != y1 ==> uy0 != uy1 // this is provable, because YUnion has been declared to be injective in its parameter

  check XUnion..getX(ux) == x
}

// DiscriminatedUnion is like a C type
//     struct {
//       Tag tag;
//       union {
//         X x;
//         Y y;
//       }
//     }
// where Tag is some type that includes the disinct values XDiscriminatedUnion..tag() and YDiscriminatedUnion..tag().

type DiscriminatedUnion
tagger Discriminant for DiscriminatedUnion
function XDiscriminatedUnion(injective getX: X): DiscriminatedUnion tag Discriminant
function YDiscriminatedUnion(injective getY: Y): DiscriminatedUnion tag Discriminant

procedure TestDiscriminatedUnion(u: DiscriminatedUnion, x: X, y0: Y, y1: Y)
{
  var ux := XDiscriminatedUnion(x)
  var uy0 := YDiscriminatedUnion(y0)
  var uy1 := YDiscriminatedUnion(y1)

  check ux != uy0 // yes, this is provable for a discriminated union
  // Here's the reason:
  check Discriminant(ux) == XDiscriminatedUnion..tag()
  check Discriminant(uy0) == YDiscriminatedUnion..tag()
  check XDiscriminatedUnion..tag() != YDiscriminatedUnion..tag()

  check y0 != y1 ==> uy0 != uy1

  check XDiscriminatedUnion..getX(ux) == x

  if Discriminant(u) == XDiscriminatedUnion..tag() {
    var xx := XDiscriminatedUnion..getX(u)
    check u != uy1
  }
}

Here is an example that defines maps from integers to values:

// This example defines maps from integers to values

type Value

type Map

function select(m: Map, i: int): Value

function store(m: Map, i: int, v: Value): Map

axiom explains select, store
  forall m: Map, i: int, j: int, v: Value
    pattern select(store(m, i, v), j)
    (i == j ==> select(store(m, i, v), j) == v) &&
    (i != j ==> select(store(m, i, v), j) == select(m, j))

procedure Test(v: Value, w: Value) {
  var m: Map

  m := store(m, 0, v)
  m := store(m, 1, w)

  check select(m, 0) == v
  check select(m, 1) == w

  m := store(m, 0, w)
  check select(m, 0) == select(m, 1)
}