N2O.PRO

SPEC

The specification is given in Anders language.

N2O

QUIC, WebSocket and MQTT embeddable protocol loop library with in-memory broker, sessions, cache, AES.GCM and Erlang Term Format serialization which is known to be faster and more efficient that JSON at server side.


  axiom pickle : Binary -> Binary
  axiom depickle : Binary -> Binary
  axiom encode : Π (k: U), k -> Binary
  axiom decode : Π (k: U), Binary -> IO k
  axiom reg: Π (k: U), k -> IO k
  axiom unreg : Π (k: U), k -> IO k
  axiom send : Π (k v z: U), k -> v -> IO z
  axiom getSession : Π (k v: U), k -> IO v
  axiom putSession : Π (k v: U), k -> v -> IO v
  axiom getCache : Π (k v: U), Atom -> k -> IO v
  axiom putCache : Π (k v: U), Atom -> k -> v -> IO v
  axiom start : PI -> IO Sup

KVS

KVS is a wrapper around RocksDB interface also compatible with SpanDB database with direct NVMe access (SPDK).


  axiom get : Π (f k v: U), f -> k -> IO (Maybe v)
  axiom put : Π (r: U), r -> IO StoreResult
  axiom delete : Π (f k: U), f -> k -> StoreResult
  axiom index : Π (f p v r: U), f -> Atom -> v -> List r
  axiom next : Reader -> IO Reader
  axiom prev : Reader -> IO Reader
  axiom take : Reader -> IO Reader
  axiom drop : Reader -> IO Reader
  axiom save : Reader -> IO Reader
  axiom append : Π (f r: U), f -> r -> IO StoreResult
  axiom remove : Π (f r: U), f -> r -> IO StoreResult

BPE

BPMN 2.0 core compliant process engine with scheduler for parallel processes and XML support compatible with Camunda Modeler.


  axiom start : Proc -> IO Sup
  axiom stop : String -> IO Sup
  axiom next : ProcId -> IO ProcRes
  axiom amend : Π (k: U), ProcId -> k -> IO ProcRes
  axiom discard : Π (k: U), ProcId -> k -> IO ProcRes
  axiom modify : Π (k: U), ProcId -> k -> Atom -> IO ProcRes
  axiom event : ProcId -> String -> IO ProcRes
  axiom head : ProcId -> IO Hist
  axiom hist : ProcId -> IO (List Hist)

NITRO

NITRO is a Nitrogen-compatible Erlang Web Framework that has no BEAM competitors (yet) in terms of speed and productivity (including not only all Erlang frameworks but also all Elixir frameworks).


  axiom q : Π (k: U), Atom -> k
  axiom qc : Π (k: U), Atom -> k
  axiom jse : Maybe Binary -> Binary
  axiom hte : Maybe Binary -> Binary
  axiom wire (actions: List Action) : IO (List Action)
  axiom render (content: Either Action Element) : Binary
  axiom insert_top (dom: Atom) (content: List Element) : IO (List Action)
  axiom insert_bottom (dom: Atom) (content: List Element) : IO (List Action)
  axiom update (dom: Atom) (content: List Element) : IO (List Action)
  axiom clear (dom: Atom) : IO Unit
  axiom remove (dom: Atom) : IO Unit

FormalTalk

FormalTalk is a Salesforce-like declarative language with limited imperative constructions designed to orchestrate N2O libraries in most effective manner. In BNF notation.


  mod     := 'module' name spec clauses
  spec    := 'kvs' | 'bpe' | 'form'
  name    := word | binary | string
  args    := [] | name args
  clause  := 'import' name
           | 'record' name args dec
           | 'notice' name args dec
           | 'event'  name args dec
           | 'route'  name args dec
           | 'form'   name args dec
  
  dec     := 'begin' decls 'end'
  clauses := clause | clause clauses
  decls   := decl | decl '|' decls
  decl    := word '=' args ':' union
           | word '=' args
           | args
           | 'document' word word '[' buttons ']' '[' fields ']'
           | 'result' '[' conts ']' args
  
  union   := args | args '+' union
  conts   := args | args '|' conts
  fields  := args | args '|' fields
  buttons := args | args '|' buttons