CMurphi入門筆記(三) 定義

2021-06-17 17:02:15 字數 2494 閱讀 9960

定義具有如下的語法:

::=    const 

| type

| var

常量定義

::=    :

常量定義中的必須有乙個在編譯的時候可以確定的值。

型別定義

::=    : 

::= -- a previously defined type.

::= .. -- integer subrange.

::= enum \ \} -- enumeration.

::= record end

::= array \[ \] of

注意,特殊的列舉型別"boolean"是預定義的,與其相關的常量"true"和"false"也是,他們均為murphi的保留字。整型型別不是預定義的,因為使用一般的整數而不將其限制為子區間將會導致儲存的急劇消耗。

簡單型別包括布林型別,列舉型別,整數的有限子區間。

復合型別是復合型別或者簡單型別的陣列,以及復合型別或者簡單型別的記錄。

陣列的索引型別必須是簡單型別。

變數定義

::=     :

下邊的例子演示了定義的**:

const 

i: 2;j: 31415 * i / 9; -- j will be 6981

type

val_t: 0..99; -- ****** types.

ind_t: 1..i;enum_t: enum ;b: boolean;r_t: record f:0..1; g: 0..2; end; -- record.

rr_t: record r: r_t; s: r_t; end; -- record of record.

a_t: array [ ind_t ] of 19..29; -- 1-dimensional array.

aa_t: array [ ind_t ] of a_t; -- 2-dimensional array.

ar_t: array [ 1..2 ] of r_t; -- array of record.

ra_t: record a1: a_t; foo: ind_t; end; -- record with array.

ae_t: array [ enum_t ] of enum_t; -- array with enum index and range.

aae_t: array [ ind_t ] of ae_t; -- 2-dim array, 2nd index is enum.

re_t: record f: enum_t; end; -- record of enum.

var val : val_t;arr : ae_t;rec : record foo: ind_t; bar: boolean; end;

所有的過程和函式都必須在程式的最外層定義,使用下邊的語法:

::=                     |     ::=    procedure \( [  ] \) ;

[ begin ] [ ] end;

::= function \( [ ] \) : ;[ begin ] [ ] end;

與pascal的過程不同,沒有引數的過程和函式仍然需要一對包含空引數的括號。

函式必須使用return語句在函式內的某處返回乙個值。函式可以有***;然後,對使用有***的函式,會有很多限制。

注:函式的***是呼叫函式的時候可以對函式之外的東西產生影響,如修改全域性變數的值,使用輸出語句(輸出到螢幕或者寫檔案等等)等等。

過程或者函式的引數列表的形式為:

::=    [var]  :

使用"var"定義的形參是通過引用傳值的;不使用"var"定義的形參也是通過引用傳值,但是在過程或者函式中不允許改變形參的值。

形參和區域性變數的定義會覆蓋他們作用域範圍之外的變數的定義。

下邊的例子展示了過程和函式的定義:

procedure swap(var i, j: val_t);var temp: val_t;begin

temp := i;i := j;j := temp;

end;function plustwo(input: val_t): val_t;const two : 2;begin

return (input + two);

end;

初看使用bnf表示的語法規則,總覺得不是很適應,不過有例子的話,就不一樣了。

傳送門:

cmurphi入門筆記(一)——概覽

cmurphi入門筆記(二)——基本概念

cmurphi入門筆記(三)——定義

介面(三)定義介面成員

第三節 定義介面成員 介面可以包含乙個和多個成員,這些成員可以是方法 屬性 索引指示器和事件,但不能是常量 域 操作符 建構函式或析構函式,而且不能包含任何靜態成員。介面定義建立新的定義空間,並且介面定義直 接包含的介面成員定義將新成員引入該定義空間。說明 1 介面的成員是從基介面繼承的成員和由介面...

三 定義主從實體基類

定義主從實體基類的原因是我希望在類的定義時,可以很明確的了解類之間的主從關係。定義primarydataentitybase 描述主從表的主表的資料實體 name id 主表實體的主鍵id name p 主表 name f 從表 public abstract class primarydataen...

微積分學習筆記三 定積分

1 介值定理 設f x 是區間 a,b 上的連續函式,那麼對於任意的u,f a u f b 或者f b u f a 在 a,b 上存在c使得f c u。2 積分中值定理 如果函式f x 在 a,b 連續,那麼在 a,b 上至少存在一點 使得 int f left x right dx f left ...