definitions.tex

%
% TeXiS
%
\def\titulo{Program Verification in Elixir}
\def\autor{Adrián Enríquez Ballester}

%
% Acronyms
%
\newacronym{api}{API}{Application Programming Interface}
\newacronym{ast}{AST}{Abstract Syntax Tree}
\newacronym{csp}{CSP}{Constraint Satisfaction Problem}
\newacronym{dialyzer}{Dialyzer}{DIscrepancy AnaLYZer for ERlang programs}
\newacronym{dsl}{DSL}{Domain-Specific Language}
\newacronym{io}{I/O}{Input/Output}
\newacronym{ir}{IR}{Intermediate Representation}
\newacronym{jvm}{JVM}{Java Virtual Machine}
\newacronym{llvm}{LLVM}{Low-Level Virtual Machine}
\newacronym{nif}{NIF}{Native Implemented Function}
\newacronym{oop}{OOP}{Object-Oriented Programming}
\newacronym{proper}{PropEr}{PROPerty-based testing tool for ERlang}
\newacronym{repl}{REPL}{Read-Eval-Print-Loop}
\newacronym{sat}{SAT}{Boolean SATisfiability problem}
\newacronym{smt}{SMT}{Satisfiability Modulo Theories}
\newacronym{ssa}{SSA}{Static Single-Assignment}
\newacronym{triq}{Triq}{Term Reductive Invariant Questant}
\newacronym{viper}{Viper}{Verification Infrastructure for Permission-based Reasoning}

%
% Commands
%
\newcommand{\true}{\ensuremath{\mathit{true}}}
\newcommand{\false}{\ensuremath{\mathit{false}}}
\newcommand{\Term}{\ensuremath{\mathit{Term}}}
\newcommand{\skipE}{\ensuremath{\textbf{skip}}}
\newcommand{\emptyE}{\ensuremath{\textbf{empty}}}
\newcommand{\failE}{\ensuremath{\textbf{fail}}}
\newcommand{\localE}{\ensuremath{\textbf{local}}}
\newcommand{\addE}{\ensuremath{\textbf{add}}}
\newcommand{\doW}{\ensuremath{\textbf{do}}}
\newcommand{\elseW}{\ensuremath{\textbf{else}}}
\newcommand{\andE}[2]{\ensuremath{#1~\textbf{and}~#2}}
\newcommand{\orE}[2]{\ensuremath{#1~\textbf{or}~#2}}
\newcommand{\blockE}{\ensuremath{\textbf{block}}}
\newcommand{\havocE}{\ensuremath{\textbf{havoc}}}
\newcommand{\assertE}{\ensuremath{\textbf{assert}}}
\newcommand{\assumeE}{\ensuremath{\textbf{assume}}}
\newcommand{\unfoldE}{\ensuremath{\textbf{unfold}}}
\newcommand{\caseE}{\ensuremath{\textbf{case}}}
\newcommand{\whenE}{\ensuremath{\textbf{when}}}
\newcommand{\ghostE}{\ensuremath{\textbf{ghost}}}
\newcommand{\Wend}{\ensuremath{\textbf{end}}}
\newcommand{\Exp}[1]{\ensuremath{\mathbf{Exp}^{#1}}}
\newcommand{\Stm}{\ensuremath{\mathbf{Stm}}}
\newcommand{\Spec}[1]{\ensuremath{\mathit{Spec}(#1)}}
\newcommand{\Defs}[1]{\ensuremath{\mathit{Defs}(#1)}}
\newcommand{\Pre}[1]{\ensuremath{\mathit{Pre}(#1)}}
\newcommand{\Post}[1]{\ensuremath{\mathit{Post}(#1)}}
\newcommand{\Pat}{\ensuremath{\mathbf{Pat}}}
\newcommand{\Body}[1]{\ensuremath{\mathit{Body}(#1)}}
\newcommand{\UserSpec}[1]{\ensuremath{\mathit{UserSpec}(#1)}}
\newcommand{\whenUnsatW}{\ensuremath{\textbf{when-unsat}}}
\newcommand{\whenUnsatE}[3]{\whenUnsatW~#1~\doW~#2~\elseW~#3}
\newcommand{\declareE}[1]{\ensuremath{\textbf{declare}~#1}}
\newcommand{\BS}[4]{\ensuremath{\langle #1,~#2,~#3\rangle \Downarrow #4}}
\newcommand{\unsat}[1]{\ensuremath{\mathit{unsat}(#1)}}
\newcommand{\isinteger}[1]{\ensuremath{\mathit{is\mbox{-}integer}(#1)}}
\newcommand{\integervalue}[1]{\ensuremath{\mathit{integer\mbox{-}value}(#1)}}
\newcommand{\isboolean}[1]{\ensuremath{\mathit{is\mbox{-}boolean}(#1)}}
\newcommand{\booleanvalue}[1]{\ensuremath{\mathit{boolean\mbox{-}value}(#1)}}
\newcommand{\tauvalue}[1]{\ensuremath{\mathit{\tau\mbox{-}value}(#1)}}
\newcommand{\taulit}[1]{\ensuremath{\mathit{\tau\mbox{-}lit}(#1)}}
\newcommand{\islist}[1]{\ensuremath{\mathit{is\mbox{-}list}(#1)}}
\newcommand{\isnelist}[1]{\ensuremath{\mathit{is\mbox{-}nonempty\mbox{-}list}(#1)}}
\newcommand{\istuple}[1]{\ensuremath{\mathit{is\mbox{-}tuple}(#1)}}
\newcommand{\istau}[1]{\ensuremath{\mathit{is\mbox{-}\tau}(#1)}}
\newcommand{\trEXP}[1]{\ensuremath{\mathit{trEXP}~\llbracket#1\rrbracket}}
\newcommand{\trExp}[2]{\ensuremath{\mathit{trExp}~#1~\llbracket#2\rrbracket}}
\newcommand{\trExps}[1]{\ensuremath{\mathit{trExp}~\llbracket#1\rrbracket}}
\newcommand{\trStm}[1]{\ensuremath{\mathit{trStm}~\llbracket#1\rrbracket}}
\newcommand{\trDef}[1]{\ensuremath{\mathit{trDef}~\llbracket#1\rrbracket}}
\newcommand{\trMatch}[2]{\ensuremath{\mathit{trMatch}~\llbracket#1\rrbracket}~\llbracket#2\rrbracket}
\newcommand{\termSize}[1]{\ensuremath{\mathit{term\mbox{-}size}(#1)}}

%
% Listings
%
\definecolor{commentgreen}{RGB}{2,112,10}
\definecolor{eminence}{RGB}{108,48,130}
\definecolor{weborange}{RGB}{255,165,0}
\definecolor{frenchplum}{RGB}{129,20,83}
\lstdefinelanguage{elixir}{
  morekeywords={case,catch,def,do,else,false,%
      use,alias,receive,timeout,defmacro,defp,%
      for,if,import,defmodule,defprotocol,%
      nil,defmacrop,defoverridable,defimpl,%
      super,fn,raise,true,try,end,with,%
      unless,defv,defparsec},
  otherkeywords={<-,->, |>, \%\{, \}, \{, \}, \, (, ), [, ], |, ::},
  morekeywords={Bool,Term,Int}
  keywordstyle = [2]{\color{frenchplum}},
  morekeywords=[2]{push,pop,declare_sort,declare_fun,assert,assume,havoc,%
      declare_const,check_sat,declare,when_unsat,add,fail,local,skip,%
      @verifier,and,or,not,requires,ensures,@spec,@type},
  sensitive=true,
  morecomment=[l]{\#},
  morecomment=[n]{/*}{*/},
  morecomment=[l][\color{purple}]{**\ (},
  morestring=[s][\color{orange}]"",
  commentstyle=\color{commentgreen},
  keywordstyle=\color{eminence},
  stringstyle=\color{red},
  basicstyle=\ttfamily,
  breaklines,
  showstringspaces=false,
  frame=tb
}

\lstdefinelanguage{dafny}{
  morekeywords={method,returns,ensures,return, int, if},
  sensitive=true,
  morecomment=[l]{\#},
  morecomment=[n]{/*}{*/},
  morestring=[s][\color{orange}]"",
  commentstyle=\color{commentgreen},
  keywordstyle=\color{eminence},
  stringstyle=\color{red},
  basicstyle=\ttfamily,
  breaklines,
  showstringspaces=false,
  frame=tb
}

\lstset{numbers=left,xleftmargin=2em,frame=single,framexleftmargin=0em,numberstyle=\footnotesize\ttfamily}
\lstset{
    literate={~} {$\sim$}{1}
}