Code

Chapter 1 edits#26

Code

Draft

gottschali wants to merge 18 commits intomainviperproject/gobra-book:mainfrom chapter-1-editsviperproject/gobra-book:chapter-1-editsCopy head branch name to clipboard

+926-471

Commits

Commits on Jan 3, 2025

• binary search for element, not inserted position

  Show description for 72c5f72
  gottschali

  committed
  72c5f72

  Copy full SHA for 72c5f72

• chore: grammar etc

  gottschali

  committed
  fb7bfc1

  Copy full SHA for fb7bfc1

• change BinarySearch to Go's signature and implementation

  Show description for 798e276
  gottschali

  committed
  798e276

  Copy full SHA for 798e276

• rewrite quantifiers

  Show description for 04a9555
  gottschali

  committed
  04a9555

  Copy full SHA for 04a9555

• simplify the final BinarySearchArr contract

  gottschali

  committed
  af42f4f

  Copy full SHA for af42f4f

• forward links for loop sections

  gottschali

  committed
  1aa79b9

  Copy full SHA for 1aa79b9

• add more context to loop invariant section

  Show description for cc81d63
  gottschali

  committed
  cc81d63

  Copy full SHA for cc81d63

• range: same linearsearch example as for invariants

  Show description for 1ea72b4
  gottschali

  committed
  1ea72b4

  Copy full SHA for 1ea72b4

• add instantiation to dict

  gottschali

  committed
  f79d907

  Copy full SHA for f79d907

• client must not be ghost function

  gottschali

  committed
  da84385

  Copy full SHA for da84385

• remove reference to old binary search

  gottschali

  committed
  9104599

  Copy full SHA for 9104599

Commits on Jan 13, 2025

• apply feedback_080125 for basic-specs

  gottschali

  committed
  a90d23b

  Copy full SHA for a90d23b

• apply feedback_080125 for basic-array

  gottschali

  committed
  91122eb

  Copy full SHA for 91122eb

Commits on Jan 15, 2025

• chore: //@ |-> // @

  gottschali

  committed
  ef41879

  Copy full SHA for ef41879

• rewrite: feedback_080125 for quantifiers

  gottschali

  committed
  d8b0e5d

  Copy full SHA for d8b0e5d

• rewrite: feedback_080125 overflow checking

  gottschali

  committed
  7e8d827

  Copy full SHA for 7e8d827

• rewrite feedback_080125 loops

  gottschali

  committed
  51fcb34

  Copy full SHA for 51fcb34

Commits on Jan 16, 2025

• rewrite based on feedback_080125 termination

  gottschali

  committed
  9114e8c

  Copy full SHA for 9114e8c