Introducing Forr?! Forr? is a tiny language that translates to Boogie. The purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie.

1 files changed, 56 insertions, 0 deletions

diff --git a/Source/Forro/Lexer.fsl b/Source/Forro/Lexer.fsl
new file mode 100644
index 00000000..b1271536
--- /dev/null
+++ b/Source/Forro/Lexer.fsl
@@ -0,0 +1,56 @@
+{

+module Lexer

+open System

+open Parser

+open Microsoft.FSharp.Text.Lexing

+}

+

+// These are some regular expression definitions

+let digit = ['0'-'9']

+let nondigit = [ 'a'-'z' 'A'-'Z' '_' ]

+let idchar = (nondigit | digit)

+let whitespace = [' ' '\t' ]

+let newline = ('\n' | '\r' '\n')

+

+rule tokenize = parse

+| whitespace    { tokenize lexbuf }

+| newline       { tokenize lexbuf }

+// operators

+| "=="          { EQ }

+| "!="          { NEQ }

+| "+"           { PLUS }

+| "-"           { MINUS }

+| "*"           { STAR }

+| "<"           { LESS }

+| "<="          { ATMOST }

+| "and"         { AND }

+| "or"          { OR }

+| "not"         { NOT }

+| "old"         { OLD }

+| "."           { DOT }

+// misc

+| "("           { LPAREN }

+| ")"           { RPAREN }

+| ";"           { SEMI }

+| ":="          { ASSIGN }

+// keywords

+| "procedure"   { PROCEDURE }

+| "requires"    { REQUIRES }

+| "ensures"     { ENSURES }

+| "do"          { DO }

+| "end"         { END }

+| "new"         { NEW }

+| "if"          { IF }

+| "then"        { THEN }

+| "else"        { ELSE }

+| "while"       { WHILE }

+| "invariant"   { INVARIANT }

+| "call"        { CALL }

+| "assert"      { ASSERT }

+// literals

+| ['-']?digit+  { INT32 (Int32.Parse(LexBuffer<char>.LexemeString lexbuf)) }

+| "null"        { NULL }

+// identifiers

+| idchar+       { ID (LexBuffer<char>.LexemeString lexbuf) }

+// EOF

+| eof   { EOF }