Accumulator
Introduction Download Case Study Contact

Case Study

In the example.zip file, there are several examples of the verified codes by the tool. For each example, there is a source code file and a .scl file. The source codes is written in a C-like language. Though their suffix is .cpp, they are not written in CPP language. However, the grammar rules are similar to C. To view the .scl files, you can open then with our scope logic tool.

The files are organized into several directories.

PreConditionDemo: Include an example to demonstrate how to calculate the weakest pre-condition for different kinds of assignments and formulas.

SimplePrograms: Include the GCD algorithm, and the algorithm to get volume by continuous plus.

ArraySort: There are several sorting algorithms, included bubble sort, heap sort, insert sort, and selection sort algorithms.

SinglyLinkedList:

  • SListInsert, which inserts a data into the list;
  • SListDelete, which deletes a node from the list;
  • SListReverse, which reverses a single linked list;
  • ListDelete-Sorted, which deletes a node from a sorted list;
  • ListInsert-Sorted, which inserts a node into a sorted list.

    • DoubleList: Include double list delete and double list insert.

    BinarySearchTree: Include the code to search, insert, delete a binary search tree.

    TopSort, which is a program to top-sorting an acyclic graph. The sorted vertexes are stored in a static list.

    SchorreWaite, which is the famous example used by many other logics. The Schorre-Wait algorithm for graph node marking.

    InvariantTestPrograms:

  • Singly-linked List, which contains programs manipulating a singly-linked list;
  • One-dimensional Array, which contains programs manipulating a one-dimensional array.
  • Two-dimensional Array, which contains programs manipulating a two-dimensional array.
  • Closed Integer Interval, which contains programs manipulating a closed integer interval.

    • WPCalculatorTestPrograms:

  • Singly-linked List, which contains programs manipulating a singly-linked list;
  • Doubly-linked List, which contains programs manipulating a doubly-linked list;
  • Static List, which contains programs manipulating a static list;
  • One-dimensional Array, which contains programs manipulating a one-dimensional array.

    		•


    ©2013 SEG NJU Homepage Introduction • Download • Case Study • Contact