MAUDE pres notes shared from AK Notepad
Below are my notes as taken by me in the Android AK Notepad tool
and shared with that tool. Note that this is exactly how they came
out when I typed them, including the stupid "smart"
capitalization.
Maude talk @galois, joe hendrix 2010.02.02
Kind & sorts, typechecking only on kinds
Only combine powerlists of same length
Cond membership needs powerlists
? Len(illformed powerlist)?
-- len() won't be applied
Head(N List) -> head(3) -> head(3 nil) -> 3
Termination: maude is indeterminate but any term has a normal form
Maude termination tool (mtt) reduces it to unsorted spec preserving non-termination
Reasoning assumes theory is confluent
Ie order of simplif preserves normal form
Confluence checker (crc)
Parameterized theories (from OBL lang)
Fth Loose semantic fmod
Need param fmod
To use param theories, need view
Meta-level is reflection module
Inductive theorem prover (itp) for reasoning over the term algebra
Uses reflection
Rewriting logic
Ops not symmetric mod not fmod
Applications
Actors, mobilemaude, duran agent lang, petri net, lambda calc, ccs, p-calc, uml diagrams, pathway logic @ sri, middleware for composable servers