SpecForge ユーザーガイド

型と式

Liloは式ベースの言語です。つまり、単純な算術から複雑な時相プロパティまで、ほとんどの構造は時系列値に評価される式です。このセクションでは、Lilo式の基本的な構成要素について詳しく説明します。

コメント

コメントブロックは/*で始まり、*/で終わります。これらのマーカー間のすべては無視されます。

行コメントは//で始まり、行の残りがコメントであることを示します。

ドキュメント文字列は//の代わりに///で始まり、さまざまな言語要素にドキュメントを添付します。

プリミティブ型

Liloは型付き言語です。プリミティブ型は次のとおりです：

• Bool： ブール値。trueとfalseが該当します。
• Int： 整数値。例：42
• Float： 浮動小数点値。例：42.3
• String： テキスト文字列。二重引用符で囲まれて書かれます。例："hello world"

型エラーは次のようにユーザーに通知されます：

def x: Float = 1.02

def n: Int = 42

def example = x + n

このドキュメントページのコードブロックは編集可能です。例えば、型エラーを修正するためにnの型をFloatに変更してみてください。

演算子

Liloは以下の演算子を使用します。優先順位の高い順（最高から最低）にリストされています。

• 前置否定：-xはxの符号反転、!xはxの否定です。

• 乗算と除算：x * y、x / y

• 加算と減算：x + y、x - y

• 数値比較：

  • ==： 等しい
  • !=： 等しくない
  • >=： 以上
  • <=： 以下
  • >： 真に大きい
  • <： 真に小さい 比較は同方向のものを連鎖させることができます。例えば0 < x <= 10は0 < x && x <= 10と同じ意味です。

• 時相演算子

  • always φ： φは将来の全ての時点で真
  • eventually φ： φは将来のある時点で真
  • past φ： φは過去のある時点で真だった
  • historically φ： φは過去の全ての時点で真だった
  • will_change φ： φは将来のある時点で値が変わる
  • did_change φ： φは過去のある時点で値が変わった
  • φ since ψ： ψが過去のある時点で真で、それ以前の全ての時点でφが真だった
  • φ until ψ： ψが真になるまでの将来の全ての時点でφが真
  • next φ： φは1つ次の（離散的な）時点で真
  • previous φ： φは1つ前の（離散的な）時点で真

  時相演算子は区間で修飾できます：

  • always [a, b] φ： a時間単位先からb時間単位先までの間の全ての時点でφが真
  • eventually [a, b] φ： a時間単位先からb時間単位先までの間のある時点でφが真
  • φ until [a, b] ψ： a時間単位先からb時間単位先までの間のある時点でψが真になり、それまでの全ての時点でφが真
  • 同様の区間修飾が他の時相演算子でも使えます。
  • 区間でinfinityを使用できます：[0, infinity]。

• 連言 x && y： xとyの両方が真

• 選言 x || y： xまたはyのいずれかが真

• 含意と等価：

  • x => y： xが真の場合、yも真でなければならない
  • x <=> y： xが真であるのは、yが真であるとき、かつそのときに限る

組み込み関数

いくつかの組み込み関数が用意されています：

• floatはIntからFloatを生成します：

  def n: Int = 42
  
  def x: Float = float(n)
  

• timeはシグナルの現在時刻を返します。

条件分岐

条件分岐を使用すると、特定の式の真偽に基づいて仕様を異なる値へと評価させることができます。if-then-else構文を使用します。

if x > 0 then "positive" else "non-positive"

Liloの重要な機能は、if/then/elseが文ではなく式であることです。つまり、常に値に評価されるため、else分岐は必須です。

if直後の式はBoolに評価される必要があります。then節とelse節は互換性のある型の値を生成する必要があります。例えば、then節がIntに評価される場合、else節もIntに評価される必要があります。

条件分岐は式が期待される場所ならどこでも使用でき、より複雑なロジックを処理するためにネストできます。

// ゼロ除算を回避
def safe_ratio(numerator: Float, denominator: Float): Float =
  if denominator != 0.0 then
    numerator / denominator
  else
    0.0 // デフォルト値を返す

// ネストされた条件式
def describe_temp(temp: Float): String =
  if temp > 30.0
    then "hot"
  else if temp < 10.0
    then "cold"
  else
    "moderate"

if _ then _ else _は時点ごと(pointwise)であることに注意してください。つまり、条件はすべての時点に独立して適用されます。

レコード

レコードは、フィールドと呼ばれる名前付きの値をグループ化する複合データ型で、仕様内で構造化データをモデル化するために不可欠です。

Lilo言語は、匿名の、構造的に型付けされた、拡張可能なレコードをサポートしています。

構築と型

中括弧で囲まれたfield = valueペアのカンマ区切りリストを提供することで、レコード値を構築できます。レコードの型は、フィールド名とそれらに対応する値の型から推論されます。

例えば、次の式は2つのフィールドを持つレコードを作成します：型Intのfooと型Stringのbar。

{ foo = 42, bar = "hello" }

結果の値は構造的型{ foo: Int, bar: String }を持ちます。コンストラクタ内のフィールドは順不同です。

type宣言を使用して名前付きレコード型を宣言することもできます。明確性と再利用性の観点から、レコード型はtype宣言で定義することを強く推奨します。

/// 2D座標系の点を表します。
type Point = { x: Float, y: Float }

// Point型の値を構築
def origin: Point = { x = 0.0, y = 0.0 }

フィールドパニング

レコードに同名で格納されるべき名前がすでにスコープ内にある場合、明示的な割り当てを省略してフィールドをパン (pun) できます。例えば{ foo }は{ foo = foo }の省略形です。

def foo: Int = 42
def bar: String = "hello"

def record_with_puns = { foo, bar }

パニングは、レコードリテラルや更新を含む、レコードフィールドがリストされる場所ならどこでも機能します。各パンは、型チェック中に通常のfield = valueペアに展開されます。

パスフィールド構築

ネストされたレコードは、ドット区切りのパスで各フィールドを記述することで、一度に作成または拡張できます。最後のフィールドに至るまでの各セグメントはその断片を含むレコードを指すものであり、コンパイラは各断片をレコード式へと適切に統合してくれます。

type Engine = { status: { throttle: Int, fault: Bool } }

def default_engine: Engine =
  { status.throttle = 0, status.fault = false }

フィールドはやはり順不同で、どのような順序で記述されていても適切なレコードにマージされます。ドット区切りのパスはパニングと組み合わせることはできません。ドット区切りのパスで指定する場合は、{ status.throttle }の代わりに{ status.throttle = throttle }と書きます。

withによるレコード更新

{ base with fields }を使用して、既存のレコードをコピーし、特定のフィールドを上書きします。更新は、レコード構築と同じ構文規則に従います：通常の割り当て、パン、ドット付きパスを混在させることができます。

type Engine = { status: { throttle: Int, fault: Bool } }

def base: Engine =
  { status.throttle = 0, status.fault = false }

def warmed_up: Engine =
  { base with status.throttle = 70 }

def acknowledged: Engine =
  { warmed_up with status.fault = false }

更新されたすべてのフィールドは、ベースレコードにすでに存在している必要があります。パス更新を使用すると、構造全体を再構築することなく、深くネストされた部分を書き換えることができます。

射影

レコード内のフィールドの値にアクセスするには、ドット（.）構文を使用します。pがxという名前のフィールドを持つレコードの場合、p.xはこの値にアクセスする式です。

type Point = { x: Float, y: Float }

def is_on_x_axis(p: Point): Bool =
  p.y == 0.0

レコードはネストでき、射影は連鎖できます。

type Point = { x: Float, y: Float }
type Circle = { center: Point, radius: Float }

def is_unit_circle_at_origin(c: Circle): Bool =
  c.center.x == 0.0 && c.center.y == 0.0 && c.radius == 1.0

ローカルバインディング

ローカルバインディングを使用すると、式に名前を割り当てることができ、その後の式で使用できます。これはletキーワードを使用して実現され、仕様の明確性、構造、効率を向上させるために非常に貴重です。

ローカルバインディングはlet name = expression1; expression2という形式をとります。これはexpression1の結果をnameにバインドします。バインディングnameは、バインディングのスコープであるexpression2内でのみ表示されます。

letバインディングの主な目的は次のとおりです：

1. 可読性：複雑な式をより小さな名前付きの部分に分割することで、ロジックを理解しやすくします。
2. 再利用：部分式が複数回使用される場合、それを名前にバインドすることで繰り返しと潜在的な再計算を回避できます。

辺の長さa、b、cから三角形の外接円の面積を計算する次の式を考えてみましょう：

def circumcircle(a: Float, b: Float, c: Float): Float =
  (a * b * c) / sqrt((a + b +c) * (b + c - a) * (c + a - b) * (a + b - c))

letバインディングを使用すると、ロジックがはるかに明確になります：

def circumcircle(a: Float, b: Float, c: Float): Float =
  let pi = 3.14;
  let s = (a + b + c) / 2.0;
  let area = sqrt(s * (s - a) * (s - b) * (s - c));
  let circumradius = (a * b * c) / (4.0 * area);
  circumradius * circumradius * pi

バインドされた変数（s、area、circumradius）の型は、それが割り当てられた式から自動的に推論されます。複数のletバインディングを連鎖させて、計算を段階的に構築することもできます。