LICENSE, README, *.md: WASM => WebAssembly, KWASM => KWasm

Everett Hildenbrandt · Everett Hildenbrandt · commit cbed41af65fa · 2019-02-25T09:04:40.000-07:00
diff --git a/LICENSE b/LICENSE
@@ -1,10 +1,10 @@
 ==============================================================================
-The WASM Semantics in K Release License
+The WebAssembly Semantics in K Release License
 ==============================================================================
 University of Illinois/NCSA
 Open Source License
 
-Copyright (c) 2009-2015 University of Illinois at Urbana-Champaign.
+Copyright (c) 2009-2019 University of Illinois at Urbana-Champaign.
 All rights reserved.
 
 Developed by:
@@ -14,7 +14,6 @@ Developed by:
 
       * University of Illinois at Urbana-Champaign (http://fsl.cs.illinois.edu/)
       * Runtime Verification, Inc (https://www.runtimeverification.com)
-      * University Alexandru-Ioan Cuza, Romania (https://fmse.info.uaic.ro)
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of
 this software and associated documentation files (the "Software"), to deal with
@@ -32,9 +31,9 @@ so, subject to the following conditions:
       documentation and/or other materials provided with the distribution.
 
     * Neither the names of the K Team, Runtime Verification, the University of
-      Illinois at Urbana-Champaign, the University Alexandru-Ioan Cuza, nor 
-      the names of its contributors may be used to endorse or promote products
-      derived from this Software without specific prior written permission.
+      Illinois at Urbana-Champaign, nor the names of its contributors may be
+      used to endorse or promote products derived from this Software without
+      specific prior written permission.
 
 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
@@ -45,16 +44,16 @@ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE
 SOFTWARE.
 
 ==============================================================================
-Copyrights and Licenses for Third Party Software Distributed with the WASM
+Copyrights and Licenses for Third Party Software Distributed with the WebAssembly
 Semantics in K:
 ==============================================================================
-The WASM Semantics in K software contains code written by third parties. 
-Licenses for this software can be found in the licenses directory 
+The WebAssembly Semantics in K software contains code written by third parties.
+Licenses for this software can be found in the licenses directory
 in the file as specified below. These files will describe the copyrights,
 license, and restrictions which apply to that code.
 
 The disclaimer of warranty in the University of Illinois Open Source License
-applies to all code in the WASM Semantics in K Distribution, and nothing in any of
-the other licenses gives permission to use the names of the K Team, Runtime
-Verification, the University of Illinois, or the University Alexandru-Ioan Cuza
+applies to all code in the WebAssembly Semantics in K Distribution, and nothing
+in any of the other licenses gives permission to use the names of the K Team,
+Runtime Verification, or the University of Illinois
 to endorse or promote products derived from this Software.
diff --git a/README.md b/README.md
@@ -1,4 +1,4 @@
-KWASM: Semantics of WebAssembly in K
+KWasm: Semantics of WebAssembly in K
 ====================================
 
 This repository presents a prototype formal semantics of [WebAssembly].
@@ -14,7 +14,7 @@ This repository generates the build-products for both backends in `.build/defn/j
 
 ### System Dependencies
 
-The following are needed for building/running KWASM:
+The following are needed for building/running KWasm:
 
 -   [git](https://git-scm.com/)
 -   [Pandoc >= 1.17](https://pandoc.org) is used to generate the `*.k` files from the `*.md` files.
@@ -74,14 +74,14 @@ This Repository
 
 ### Semantics Layout
 
-The following files constitute the KWASM semantics:
+The following files constitute the KWasm semantics:
 
--   [data.md](data.md) provides the (functional) data of WASM (basic types, type constructors, and values).
--   [wasm.md](wasm.md) is the main KWASM semantics, containing the configuration and transition rules of WebAssembly.
+-   [data.md](data.md) provides the (functional) data of WebAssembly (basic types, type constructors, and values).
+-   [wasm.md](wasm.md) is the main KWasm semantics, containing the configuration and transition rules of WebAssembly.
 
 These additional files extend the semantics to make the repository more useful:
 
--   [test.md](test.md) is an execution harness for KWASM, providing a simple language for describing tests/programs.
+-   [test.md](test.md) is an execution harness for KWasm, providing a simple language for describing tests/programs.
 
 ### Example usage: `./kwasm` runner script
 
diff --git a/data.md b/data.md
@@ -1,5 +1,5 @@
-WASM Data
-=========
+WebAssembly Data
+================
 
 ```k
 require "domains.k"
@@ -13,7 +13,7 @@ Parsing
 
 ### Layout
 
-WASM allows for block comments using `(;` and `;)`, and line comments using `;;`.
+WebAssembly allows for block comments using `(;` and `;)`, and line comments using `;;`.
 Additionally, white-space is skipped/ignored.
 Declaring regular expressions of sort `#Layout` infroms the K lexer to drop these tokens.
 
@@ -26,7 +26,7 @@ Declaring regular expressions of sort `#Layout` infroms the K lexer to drop thes
 
 ### Identifiers
 
-As defined in the [WASM Spec], the syntax of identifiers is as follows.
+As defined in the WebAssembly spec, the syntax of identifiers is as follows.
 
 **TODO**: Unsupported characters: `.:^@`
 
@@ -35,12 +35,12 @@ As defined in the [WASM Spec], the syntax of identifiers is as follows.
  // ------------------------------------------------------------------------
 ```
 
-WASM Types
-----------
+WebAssembly Types
+-----------------
 
 ### Base Types
 
-WASM has four basic types, for 32 and 64 bit integers and floats.
+WebAssembly has four basic types, for 32 and 64 bit integers and floats.
 
 ```k
     syntax IValType ::= "i32" | "i64"
@@ -106,7 +106,7 @@ Values
 
 ### Basic Values
 
-WASM values are either integers or floating-point numbers, of 32- or 64-bit widths.
+WebAssembly values are either integers or floating-point numbers, of 32- or 64-bit widths.
 
 ```k
     syntax Number ::= Int | Float
@@ -169,7 +169,7 @@ Function `#bool` converts a `Bool` into an `Int`.
 Data Structures
 ---------------
 
-WASM is a stack-machine, so here we provide the stack to operate over.
+WebAssembly is a stack-machine, so here we provide the stack to operate over.
 Operator `_++_` implements an append operator for sort `Stack`.
 
 ```k
@@ -201,8 +201,3 @@ Operator `_++_` implements an append operator for sort `Stack`.
     rule #drop(TYPE VTYPES, < TYPE > VAL:Number : STACK) => #drop(VTYPES, STACK)
 endmodule
 ```
-
-Resources
-=========
-
-[WASM Spec]: <https://github.com/WebAssembly/design>
diff --git a/kwasm b/kwasm
@@ -104,11 +104,11 @@ case "$run_command-$backend" in
     usage: $0 (run|test) [--backend (ocaml|java|haskell)] <pgm>  <K args>*
            $0 prove      [--backend (java|haskell)]       <spec> <K args>*
 
-       $0 run   : Run a single WASM program
-       $0 test  : Run a single WASM program like it's a test
-       $0 prove : Run a WASM K proof
+       $0 run   : Run a single WebAssembly program
+       $0 test  : Run a single WebAssembly program like it's a test
+       $0 prove : Run a WebAssembly K proof
 
-       Note: <pgm> is a path to a file containing a WASM program.
+       Note: <pgm> is a path to a file containing a WebAssembly program.
              <spec> is a K specification to be proved.
              <K args> are any arguments you want to pass to K when executing/proving.
 " ; exit ;;
diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md
@@ -1,7 +1,7 @@
 KWASM Lemmas
 ============
 
-These lemmas aid in verifying WASM programs behavior.
+These lemmas aid in verifying WebAssembly programs behavior.
 They are part of the *trusted* base, and so should be scrutinized carefully.
 
 ```k
diff --git a/test.md b/test.md
@@ -1,4 +1,4 @@
-KWASM Testing
+KWasm Testing
 =============
 
 For testing, we augment the semantics with some helpers.
diff --git a/wasm.md b/wasm.md
@@ -1,5 +1,5 @@
-WASM State and Semantics
-========================
+WebAssembly State and Semantics
+===============================
 
 ```k
 require "data.k"
@@ -44,7 +44,7 @@ Instructions
 
 ### Sequencing
 
-WASM instructions are space-separated lists of instructions.
+WebAssembly instructions are space-separated lists of instructions.
 
 ```k
     syntax Instrs ::= List{Instr, ""} [klabel(listInstr)]
@@ -419,7 +419,7 @@ It simply executes the block then records a label with an empty continuation.
 The `br*` instructions search through the instruction stack (the `<k>` cell) for the correct label index.
 Upon reaching it, the label itself is executed.
 
-Note that, unlike in the WASM specification document, we do not need the special "context" operator here because the value and instruction stacks are separate.
+Note that, unlike in the WebAssembly specification document, we do not need the special "context" operator here because the value and instruction stacks are separate.
 
 ```k
     syntax Instr ::= "(" "br" Int ")"

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KWASM Testing`
	`1`	`+KWasm Testing`
`2`	`2`	`=============`
`3`	`3`
`4`	`4`	`For testing, we augment the semantics with some helpers.`