[學不動系列]Libra Move白皮書-語法介紹
接著上一篇：基本介紹， 本節介紹Move的語法，同時從語法我們可以看出Move在安全方面的考慮。
白皮書使用了一種半形式化(semi-formal)的描述語言進行了描敘。至於這套描述語言，主要符號解釋如下（如有不準確，請告知）：
- =： 定義
- ::= ： 賦值
- ?： 映射
- ×： product type，也就是表示結構體
- ∈： 表示屬於某個類型或者集合中的一個元素
通過這些符號，Move定義了如下的語法類型：
Global state： 地址到賬戶的map，賬戶由Resource和Module構成。形式化定義如下：
Modules：由名字，結構體聲明以及過程聲明組成, 可以簡單理解為c++的class。module通過ModuleId被外部索引（訪問），結構體通過structId被外部索引，結構體聲明是一個<kind, FieldName->非引用類型>的product類型。
Module定義了資源的作用域，類似於c++的namespace的功能。其中Module內置了幾個重要的函數用來進行類型操作：
- Pack and Unpack 用於從非受限類型創建和銷毀模塊的資源；
- MoveToSender/MoveFrom 在當前賬戶地址下面發布或者刪除對應的資源；
- BorrowField ：獲得結構體的一個欄位的引用
Types: 包含基本類型（bytes是fixed-size字元串，AccountAddress是256bits），結構體類型，非引用類型，以及
在Module裡面除去被聲明為資源的類型（標記了resource kind），其餘的類型統稱為unrestricted types（不受限類型）。資源類型的變數或者欄位只能被move，並且資源類型變數的引用不能被解引用，也不能被重複賦值。另外an unrestricted struct不能包含restricted field，原因很簡單， unrestricted 結構體被賦值或者複製的時候，如果有restricted欄位，那這個欄位不會實際被操作到。
Values：
Move支持引用，引用是短暫的，因此不能被用來定義結構體的欄位，也不能引用引用，應用的聲明周期就是交易腳本的執行過程。通過Borrow{Loc, Field, Global}可以分別可以獲得局部變數，結構體變數或者全局變數的引用（敲黑板，請學習rust）。
另外因為struct里不能存儲reference，所以可以保證struct一定是一個tree而不會有backedge。這也是move比rust簡化的最重要的一點，正因此move不需要複雜的lifetime。 因此Resource同樣也不可能出現圖結構。這樣確實大大簡化了語言的處理。
Procedures and transaction scripts：
過程的簽名包含函數的訪問控制修飾符，參數類型和返回值類型。過程聲明包括一個過程簽名，局部變數和一系列的指令，（作者認為，這個聲明理解為定義（definition）更合適一些）。一個交易腳本是一個不關聯具體module的過程，因此他不會被複用，交易腳本操作的全局狀態轉換，這些狀態的修改要麼全部成功，要麼全部失敗。
ProcedureID標識一個過程，被moduleId和過程簽名唯一確定，並且Call指定將其作為第一個參數，進行調用。這也就意味著函數調用是靜態可確定（staticly determined）的，不存在什麼函數指針或者函數表。同時模塊內的過程依賴是無環的，加上模塊本身的沒有動態指派，這樣就加強了執行期間的函數調用的不可變性：也就是一個procedure在執行過程的call frame必然是相鄰的。因此也防止了類似於以太坊裡面的re-entrancy攻擊（這個就是有名導致分叉出ETC的攻擊）。
下一節介紹Move的解釋器。
推薦閱讀：
