MiGo types library in Go
Switch branches/tags
Clone or download
Latest commit 71ed587 Nov 28, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
mock_migo
.gitignore
.travis.yml
Gopkg.lock
Gopkg.toml
LICENSE
README.md
doc.go
errors.go
example_test.go
lexer.go
migo.go
migo.y
migo_test.go
parser.y.go
scanner.go
stack.go
stack_test.go
token.go
var.go

README.md

migo Build Status GoDoc

nickng/migo is a MiGo Types library in Go.

MiGo (mini-go) calculus is a introduced in this paper to capture core concurrency features of Go.

This library was designed to work with MiGo types, i.e. the types of communication primitives in the MiGo calculus, where the values to be sent/received are abstracted away, for static analysis and verification.

Install

The package can be installed using go get:

go get github.com/nickng/migo

Some tests uses golang/mock, to (re)generate mock files, install mockgen and run go generate:

go get github.com/golang/mock/mockgen
go generate
go test

MiGo types

Syntax:

identifier = [a-zA-Z0-9_.,#/]
digit      = [0-9]
program    = definition* ;
definition = "def " identifier "(" param ")" ":" def-body ;
param      =
           | params
           ;
params     = identifier
           | params "," identifier
           ;
def-body   = def-stmt+
           ;
prefix     = "send" identifier
           | "recv" identifier
           | "tau"
           ;
def-stmt   = "let" identifier = "newchan" identifier, digit+ ";"
           | prefix ";"
           | "close" identifier ";"
           | "call"  identifier "(" params ")" ";"
           | "spawn" identifier "(" params ")" ";"
           | "if" def-stmt+ "else" def-stmt+ "endif" ";"
           | "select" ( "case" prefix ";" def-stmt* )* "endselect" ";"
           ;

Verification of MiGo

Gong is a liveness and safety checker of MiGo types. The tool accepts MiGo types format generated by this package.