形式仕様記述における探索的モデリング

(1)

Kyushu University Institutional Repository

形式仕様記述における探索的モデリング

小田, 朋宏

https://doi.org/10.15017/1866375

出版情報：Kyushu University, 2017, 博士（工学）, 論文博士バージョン：

権利関係：

(2)

(3)

(4)

2

ViennaTalk ViennaTalk VDM-SL

Smalltalk

Web IDE

VDMPad UI Lively Walk-Through Web API

Webly Walk-Through ViennaTalk VDM

ViennaTalk

(5)

(6)

1 1

1.1 . . . . 1

1.2 . . . . 2

1.3 . . . . 3

1.4 . . . . 4

1.5 VDM-SL . . . . 6

1.6 . . . . 8

2 9 2.1 . . . . 9

2.1.1 . . 10

2.2 . . . . 11

2.2.1 . . . . 12

2.2.2 . . . . 12

2.3 . . . . 13

2.3.1 . . . . 13

2.3.2 . . . . 16

2.4 . . . . 18

2.5 . . . . 21

2.5.1 . . . . 21

2.5.2 . . . . 23

2.5.3 33 2.5.4 . . . . 37

2.6 . . . . 39

3 41 3.1 . . . . 41

3.1.1 41

(7)

3.2 . . . . 45

3.3 . . . . 48

3.3.1 . . . . 48

3.3.2 . . . . 49

3.3.3 . . . . 49

3.3.4 . . . . 50

3.3.5 . . . . 51

3.3.6 . . . . 51

4 ViennaTalk 53 4.1 . . . . 53

4.2 . . . . 55

4.3 ViennaTalk . . . . 63

4.3.1 Animation . . . . 65

4.3.2 Browser . . . . 65

4.3.3 Value . . . . 69

4.3.4 Type . . . . 72

4.3.5 Engine . . . . 73

4.3.6 Parser . . . . 75

4.3.7 . . . . 77

4.4 VDMPad . . . . 86

4.4.1 . . . . 88

4.4.2 VDM-SL . . . . 91

4.4.3 . . . . 92

4.4.4 . . . . 93

4.5 Lively Walk-Through . . . . 94

4.6 Webly Walk-Through . . . . 97

5 ViennaTalk 101 5.1 . . . . 101

5.1.1 . . . . 102

5.1.2 . . . . 104

5.2 VDMPad . . . . 106

5.3 ViennaTalk . . . . 109

(8)

6.1.1 . . . . 114

6.1.2 . . . . 115

6.1.3 . . . . 116

6.1.4 . . . . 116

6.1.5 . . . . 116

6.2 7 . . . . 117

6.3 . . . . 119 121 122 122 129 132

(9)

(10)

1

VDM-SL

1.1

(11)

[AL98, IPA13]

1.2

[FLS08, AL98, WLBF09, KN09, IPA13]

1

[Tas02]

[IPA13]

(12)

[RW73]

1.3

(13)

ViennaTalk ViennaTalk

1.4

Fitzgerald

VDM-SL [FJ98]

1.

2.

3.

4.

5.

6.

7.

VDM-SL 1 1

[ADL⁺91, Abr07]

Z [Spi92] B-method[ADL⁺91] event-B[Abr07]

3

•

(14)

•

1 (Abstract

Machine)

[Rob95]

[IPA13, VTSHO12]

[DNBM12]

eXtreme Programming Scrum

XFM [SMSB05]

[BBB⁺09]

(15)

2

1.5 VDM-SL

VDM-SL[FJ98] VDM++[FLM⁺05] VDM-RT[Ver09] Z [Spi92] B-method[ADL⁺91] event-B[Abr07] Larch[Gut91]

OBJ[GT79] UML

VDM-SL VDM++ Z

Larch OBJ

VDM-SL VDM++

VDM-RT VDM (Vienna Development Method)

VDM-SL (VDM Specification Language)

VDM-SL 1996

(16)

Z

VDM-SL

VDM++ VDM-SL

C++

VDM-RT VDM++ CPU

VDM-SL VDM++

VDM-SL

3 [BH95, 08]

0 : 1 : 2 : 0

1

Z B-method

event-B

(Correctness by Construction) 1

2 1 1

VDM-SL

(17)

1.6

2

3

4

ViennaTalk 3

ViennaTalk

5 ViennaTalk ViennaTalk

VDMPad ViennaTalk

ViennaTalk

6

(18)

2

2.1

(well-defined

problem) (ill-defined problem, wicked prob-

lem) [RW73, Sim96, FR92, AEF97]

A B

(19)

[RW73]

[Fis05]

2.1.1

(20)

2.2

[Fis94]

(21)

2.2.1

2.2.2

1 UI

[IPA13]

(22)

2.3

2.3.1 IEEE 830-1998

2.3.2

2.3.1

IEEE 830-1998

IEEE 830-1998 2.1

(23)

2.1: IEEE 830-1998 (correctness)

(unambiguity) (completeness)

(consistency) (ranked)

(verifiability) (modifiability) (traceability)

(24)

(well-formedness) (correctness)

(feasibility)

(operational-completeness)

(total-definition) (consistency)

(verifiability) (modifiability)

2.1

2.2

2.2 2.1

(well-formedness) 2.1

(25)

2.1 2.1

2.1

2.3.2

VDM-SL

[IPA13]

(26)

(reflection in action)[Sch84]

(27)

⇥⇤⌅

⇧⌃⌥ ⌦↵

✏⇣⌘✓◆

1. ⌫⇠⇡⇢

⌧

2. !"#⇣$%&

'()* ⌧

⇤⌅+,-. ⇥⇤⌅' +,⌦↵

⇤⌅+,-.

/01⇢23456⇢

✏⇣⌘✓◆' 78⌦↵

⇤⌅+,-.

/01⇢234

⇥⇤⌅⇢9:';<⌦↵

/01⇢234

⇤⌅+,-.

⇥⇤⌅'=>⌦↵

⇤⌅+,-

2.1:

2.4

2.1

(28)

UI UI

2.1

2 1

1 VDM-SL

VDM-SL VDM-SL

(29)

2.3:

2.3

(30)

2.5

2.5.1

2.2

(31)

⇥⇤

⌅⇧⌃⌥ ⌦↵

✏⇣⌘ ⇥⇤✓

◆  ✏⇣⌘

⌫⇠ ⇡⌅⇧⌃⌥

10 50 100

⇢ ⌧ ⇧⌃

◆ !"

◆  ✏⇣ #$%

◆ !"&'()⇡

◆ !"*'(&

+,)⇡

- ./%

◆ !"&'()⇡

⌅⇧⌃⌥

01⌘2203

4⌦5&6 7) 85⇥9 ⇧⌃

2.2:

(32)

1

20

2.5.2

VDM-SL

(33)

✞module

imports from operations ;

exports all definitions

✡✝ ✆

2.1:

2.1

VDM-SL

(34)

✞types

= < >| < >| < >;

= nat;

= map to ;

= nat;

values

= {< > |-> 100, < > |-> 50,

< > |-> 10};

= 20;

state State of : :

inv mk_State( , -) ==

forall in set dom &

( ) <= --

init s == s = mk_State(

{< > |-> 0, < > |-> 0, < > |-> 0}, 0)

✡✝end ✆

2.2:

(35)

VDM-SL

types values functions

state operations

state 1

1

VDM-SL

VDM-SL types values

state 2.2

2.2 types values

2.2

✞types

= nat;

:: :nat;

✡✝ ✆

mk (500) mk (123)

(36)

2.1

1 3 {<

> |-> 1, < > |-> 3} 80

2.2 {< >

|-> 1, < > |-> 3} {< > |-> 0, <

> |-> 1, < > |-> 3}

1 3 nat1

inv == 0 not in set rng {< > |-> 1, <

> |-> 3} 1 3

inv ==

dom = {< >, < >, < >}

{< > |-> 0, < > |-> 1,

< > |-> 3} 1 3

2.2

(1) (2)

(3) (4)

values

(37)

1 state

inv

init 0

2.3

3

2.4

2.4 pure pure

pure

(38)

✞operations

: () ==> ()

() == (< >);

: () ==> ()

() == (< >);

: () ==> ()

() == (< >);

: () ==> () () ==

let

:[ ] = ( )

in

if <> nil

then

( ( );

:= 0;

‘ ());

: () ==> () () == skip;

✡✝ ✆

2.3:

(39)

✞

pure : ==> [ ]

( ) ==

(dcl : := ,

:map to := {|->};

for in

do if

in set dom then

let

: =

min( ( ),

div ( ))

in

( ( ) := ;

:=

- ( ) * );

return if = 0 then else nil);

✡✝ ✆

2.4:

nil nil

2 2.5

:= -

nat -

>= 0 <=

✞operations

pure : () ==>

() == return ;

: ==> ()

( ) == := -

pre <= ;

✡✝ ✆

2.5:

(40)

✞functions

min : nat * nat -> nat

min(x, y) == if x <= y then x else y;

operations

: ==> ()

( ) ==

( ( )

:= min( ( )+1, );

:= + ( );

‘ ());

✡✝ ✆

2.6:

2.6 min

2.1

VDM-SL

VDM-SL 2.1

(41)

✞values

= [< >, < >, < >];

operations

: ==> ()

( ) ==

(for all in set dom do

for i = 1 to ( )

do

cases :

< > -> (),

< > -> ()

end;

:= ({ |-> ( )- ( )

| in set dom }

munion dom <-: ))

pre

dom subset dom

and (forall in set dom &

( ) >= ( ));

✡✝end ✆

2.7:

(42)

( ) ==

( ( ) := ;

‘ ());

✡✝ ✆

2.8:

2.5.3

2.8

(43)

✞

: () ==> () () ==

( ( ( ));

:= 0;

‘ ()));

✡✝ ✆

2.9:

✞state State of : :

inv mk_State( , ) ==

(forall in set dom &

( ) <= ) --

and ( , ) <> nil --

{< |-> 0, < > |-> 0, < > |-> 0}, 0)

✡✝end ✆

2.10:

100 1 1

80 20

2 2.3

2.9

( ) nil

2.10 2.10

2.11

(44)

(dcl : := ,

:map to := {|->};

for in do

if in set dom

then let

: =

min( ( ),

div ( ))

in

if > 0

then

( :=

munion { |-> };

:=

- ( ) * );

return if = 0 then else nil);

pure : ==> [ ]

( ) ==

return ( , );

✡✝ ✆

2.11:

2.10

2.4

2.11 2.11

2.4

2.11

(45)

✞operations

: ==> ()

( ) == := -

pre <=

and ( , - ) <> nil;

: ==> ()

( ) ==

(dcl

: := ,

: := + ( );

( )

:= (if in set dom

then ( )

else 0) + 1;

if

( ) > ( )

then

( ) := ( );

if

( , ) <> nil

then

(atomic (

:= ;

:= );

‘ ()));

✡✝ ✆

2.12:

2.10

2.12

(46)

1

3 LED

3

2.13 2.1

VDM-SL

2.5.4

(47)

✞values

= 999;

state State of : :

inv mk_State( , ) ==

(forall in set dom &

( ) <= ) --

and ( , ) <> nil --

and <= --

{< |-> 0, < > |-> 0, < > |-> 0}, 0)

end

operations

: ==> ()

( ) ==

(dcl

: := ,

: := + ( );

( )

:= (if in set dom

then ( )

else 0) + 1;

if

( ) > ( )

then

( ) := ( );

if ( , ) <> nil

and <=

then

(atomic (

:= ;

:= );

‘ ()));

✡✝ ✆

2.13:

(48)

2.4

2.6

3.2

(49)

(50)

3

3.1

2.4

2

3.1.1

3.1

1

(51)

⇥⇤⌅

⇧⌃⌥ ⌦↵

✏⇣⌘✓◆

⌫⇠⇡⇣⇢ ⌧ !"#$

%&'()*+

⇤⌅,-.

⇤⌅,-./

%&'()*+

⇥⇤⌅(01 23⌦↵

456782

⇤⌅,-./

%&'()*+9:(

✏⇣⌘✓◆

;<⌦↵

456781

3.1:

(52)

2

3.1.2

3.2

3

(53)

⇥⇤⌅

⇧⌃⌥ ⌦↵

✏⇣⌘✓◆

⌫⇠⇡⇢⌧

!⇢"#$

⇤⌅%&'

⇤⌅%&'(

⇥⇤⌅)%&⌦↵

*+,-.4

⇤⌅%&'(

⇥⇤⌅)/0⌦↵

*+,-.3

3.2:

(54)

4

3

3.2

3.1

1

(55)

2

[Fis94]

(56)

[Fis94]

3

(57)

4

3.3

3.2

3.3.1

3

4

(58)

3.3.2

4

3

3.3.3

VDM-SL

(59)

UI

2

VDM vdmUnit [LLJ⁺13]

[LLB10]

3.3.4

[OA93]

1

(60)

3.3.5

B-method VDM-SL

(code generator) (transpiler)

3

2

3.3.6

(61)

eXtreme Programming

VDM vdmUnit [LLJ⁺13]

3 4

(62)

4 ViennaTalk

4.1

ViennaTalk 4.1 ViennaTalk Pharo

Smalltalk [BDN⁺09] ViennaTalk

VDMJ [Bat09]

VDMJ VDM-SL

VDM++ VDM-RT Java JRE

(Java Runtime Environment) ViennaTalk

JavaScript

ViennaTalk Pharo Smalltalk

Smalltalk [Kay72]

Kay

Smalltalk

(63)

⇥⇤⌅⇧⌃ ⇥⇤⌅⇧⌃

OS OS

Pharo Smalltalk

JRE ⌅⇧⌥⌥ ⌅

ViennaTalk

VDMPad

VDMJ Engine

4.1: ViennaTalk

Smalltalk

Smalltalk Smalltalk Smalltalk

Smalltalk sUnit

sUnit Kent Beck

sUnit xUnit

1.4

eXtreme Programming [Ola03]

Pharo Smalltalk

Smalltalk [BDN⁺09] Smalltalk

Morphic [MS95, IKM⁺97]

3.2

• 1

(64)

• 2

• 3

• 4

Pharo Smalltalk

1 2

DSL

sUnit Pharo Smalltalk

3 4

4.2

3.2 ViennaTalk

1

ViennaTalk

(65)

4.2

State1

Op1 State2

State1’ State2

State1’ Op1 State2’

Op2

State3’ State1

Op1 State2

State2 State2” Op2

State3”

(66)

State1 State2

State1' State2'

Op1

State3'

仕様アニメーション

編集

非ライブな

仕様アニメーション

ライブな

仕様アニメーション

Op1 Op2

State1 State2

State2''

Op1

State3'' Op2 編集

仕様アニメーション

4.2:

(67)

VDM-SL

ViennaTalk 1 4.3

Smalltalk

(68)

ファイルシステム

ファイルベース環境

イメージベース環境

/ 開発環境

usr/

/bin /lib home/

johndoe/

src/

spec1.vdmsl spec2.vdmsl spec1.cpp

開発環境

エディタオブジェクトアニメーションオブジェクト

エディタ

インタプリタソース

ツリー

文字列（仕様記述）

リスト（状態）

エディタオブジェクトエディタオブジェクト

4.3:

(69)

ViennaTalk Pharo Smalltalk ViennaTalk

2

ViennaTalk VDM-SL 2

1 HTML 1

Smalltalk VDM-SL

ViennaTalk VDM-SL HTML

ViennaTalk VDM-SL VDM-SL

1 VDM-SL

GUI 4.5

Lively Walk-Through VDM-SL GUI

UI ViennaTalk

Pharo Smalltalk Morphic [MS95, IKM⁺97] GUI

(Graphical User Interface) Lively Walk-

Through GUI Morphic

GUI

Lively Walk-Through VDM-SL

Smalltalk VDM-SL

Smalltalk

ViennaTalk VDM-SL Smalltalk

(70)

1 VDM-SL Smalltalk at: at:put:

Smalltalk

Smalltalk VDM-SL

Smalltalk

VDM-SL Smalltalk

4.3.7 ViennaTalk

VDM-SL Smalltalk

GUI VDM-SL

ViennaTalk

VDM-SL VDM-SL

HTML

Lively Walk-Through GUI GUI

VDM-SL Smalltalk Smalltalk

3

(71)

4.1: ViennaTalk

ViennaTalk

VDM-SL VDMTools Overture tool

ViennaTalk

VDM VDMJ

4 ViennaTalk

(72)

ViennaTalk IDE VDMPad VDM-SL

VDMPad VDM-SL

Pharo Smalltalk VDM-SL

VDM-

SL Smalltalk Pharo Smalltalk

4.3 ViennaTalk

ViennaTalk 4.4 4.4

1

Engine Zinc

(73)

Engine

Lively Walk-Through

Parser

Webly Walk-Through

Type Animation

VDMPad Value

VDMBrowser Zinc

OSProcess NeoJSON

PetitParser

⇥⇤

⌅⇧⌃

ViennaTalk

4.4: ViennaTalk Smalltalk

Type

Value Engine

Pharo Smalltalk

Metacello ViennaTalk

ViennaTalk

(74)

Animation VDM-SL ViennaAnimation VDM-SL

VDM-SL VDM-SL

VDM-SL

ViennaTalk VDMBrowser Lively Walk-Through

4.3.2 Browser

Browser VDM-SL

VDMBrowser ViennaBrowser VDM-

Browser 4.2 1

IDE VDMBrowser Animation

VDMBrowser

VDM-SL VDM-SL

4.5 VDMBrowser VDMBrowser UI

2 UI

Specification VDM-SL

Workspace

(75)

4.5: VDMBrowser

(76)

4.6: VDMBrowser Workspace

(77)

VDM-SL 1 VDMBrowser

1

VDM-SL

VDM-SL VDM-SL

VDM-SL

VDM-SL VDMBrowser

4.3.7 (Transpiler)

VDM

ViennaTalk Smalltalk

Smalltalk

Smalltalk Smalltalk

Smalltalk

(78)

ViennaTalk VDMBrowser Smalltalk

VDM-SL

Smalltalk VDM-SL

4.3.3 Value

ViennaTalk VDM-SL Smalltalk

Value

VDM-SL Smalltalk

4.2 VDM-SL Smalltalk 4.3

VDM-SL 4.4 Smalltalk

VDM-SL Smalltalk

VDM-SL

VDM-SL Smalltalk

VDM-

SL ViennaTalk

ViennaRuntimeUtil 4.3.4

(79)

4.2: VDM-SL

VDM-SL Smalltalk

nat Integer

nat1 Integer

int Integer

real Float

bool Boolean

<quote> Symbol

t1*t2 Array

set oft Set

seq oft OrderedCollection mapt1tot2 Dictionary

inmapt1tot2 Dictionary t1-> t2 BlockClosure

token ViennaToken

composetof ViennaComposite f1:t1

f2:-t2 t3end

4.3: VDM-SL

VDM-SL ViennaComposite

ViennaToken ViennaComposition ViennaIteration ViennaException

(80)

4.4: VDM-SL

Context viennaReturn:value

return Collection onlyOneSatisfy:block block

1

power

powerDo: block

block OrderedCollection,

Dictionary, BlockClosure

applyTo: value value Dictionary, BlockClosure comp: map-or-func

**value value

(81)

[VBLN11] ViennaStateSlot

ViennaStateSlot

ViennaStateInvariantViolation

4.3.4 Type

Type VDM-SL

Smalltalk

Smalltalk VDM-SL

VDM-SL ViennaTalk

VDM-SL 1

ViennaTalk 1

ViennaType VDM-SL

ViennaNat VDM-SL

4.5 VDM-SL Vien-

naTalk ViennaTalk

4.2

4.5 VDM-SL

1 ViennaTalk SmallInteger

nat ViennaTalk ViennaType nat

ViennaNat ViennaType nat

incliudes: 1 Smalltalk VDM-SL 1

VDM-SL nat ViennaNat

ViennaType nat SmallInteger

1 includes:

SmallInteger ViennaNat ViennaTalk Smalltalk VDM-SL

(82)

<=

do:

inv: 4.5 Smalltalk

optional *, |, set

API ViennaNat

VDM-SL API

4.3.5 Engine

Engine VDM-SL

ViennaTalk VDM-SL Java

VDM VDMJ [Bat09] VDM

VDM-SL En-

gine ViennaEngine ViennaVDMJ ViennaClient ViennaBankEngine ViennaServer 5

ViennaEngine VDM

API evaluate: specification:

states: module: vdm10: rtc: 4.6

API ViennaEngine

API

nil nil

ViennaVDMJ VDMJ

VDM-SL MacOS

Linux

Pharo Smalltalk Windows

ViennaClient VDM

HTTP

(83)

4.5: VDM-SL

VDM-SL

Smalltalk

nat ViennaType nat ViennaNatType

nat1 ViennaType nat1 ViennaNat1Type

int ViennaType int ViennaIntType

real ViennaType real ViennaRealType

bool ViennaType bool ViennaBoolType

<quote> ViennaType quote: #quote ViennaQuoteType

[t] toptional ViennaOptionType

t1*t2 t1*t2 ViennaProductType

t1|t2 t1|t2 ViennaUnionType

set oft tset ViennaSetType

set1 oft tset1 ViennaSet1Type

seq oft tseq ViennaSeqType

seq1 oft tseq1 ViennaSeq1Type

mapt1tot2 t1mapTo: t2 ViennaMapType

inmapt1tot2 t1inmapTo: t2 ViennaInmapType

t1-> t2 t1-> t2 ViennaPartialFunctionType t1+> t2 t1+> t2 ViennaTotalFunctionType

token ViennaType token ViennaTokenType

composetof ViennaType compose: ’t’ of: ViennaCompositeType f1: t1 {f1. false .t1.

f2:-t2 {f2. true .t2}. t3end {nil . false . t3}}

tinvpattern==expr tinv: [:v|expr] ViennaConstrainedType

(84)

expression String

specification String

states Dictionary

module String

vdm10 VDM Boolean

rtc Boolean

result Object nil

states Dictionary

message String nil

URL Windows

ViennaBankEngine

ViennaVDMJ VDM

ViennaClient VDM

ViennaServer VDM

ViennaServer ViennaEngine

HTTP 16 ViennaVDMJ

4.3.6 Parser

Parser VDM-SL ViennaVDMParser

(AST) ViennaNode

(85)

ViennaVDMGrammar

ViennaVDMParser

ViennaVDMValueDecoder ViennaVDMHighlighter VDM source

VDM AST

ViennaVDMFormatter

ViennaVDM2Smalltalk

ViennaVDM2SmalltalkClass ViennaVDM2SmalltalkObject

ViennaVDM2SmalltalkScript

Smalltalk

⇥⇤⌅⇧⌃

Smalltalk

⇧⌥

Smalltalk

⇥⇤⌅⇧⌃

Smalltalk

⇧ ⌦⌃

4.7:

PEG (Parser Expression Grammar) PetitParser 4.7

ViennaVDMGrammar VDM-SL

ViennaVDMParser ViennaVDMGrammar

ViennaVDMHighlighter VDM-SL ViennaVDMHighlighter

ViennaVDMGrammar

(86)

Smalltalk ViennaVDMValueDecoder ViennaVDMGrammar

VDM-SL ViennaVDMFormatter ViennaVDMParser

VDM-SL ViennaVDMFormatter

ViennaTalk VDM-SL

VDM-SL Smalltalk

3 ViennaVDM2SmalltalkScript

VDM-SL Smalltalk

VDM-SL

ViennaVDM2SmalltalkClass VDM-SL

Smalltalk VDM-SL

ViennaVDM2SmalltalkObject VDM-SL

Smalltalk ViennaVDM2SmalltalkObject

Smalltalk

VDM-SL

4.3.7

(87)

ViennaTalk

VDM

VDMTools

C++ Java Overture tool

Java

VDM

3.2

1-a 1-d

3.2 1 ViennaTalk

(88)

4 1-a

ViennaTalk

Smalltalk ViennaTalk

1-b Vien-

naTalk

ViennaTalk

1-c VDM-SL

ViennaTalk

VDM-SL Smalltalk

1-d

(89)

Smalltalk

2

ViennaTalk Smalltalk GUI

3

4

ViennaTalk Smalltalk Pharo Smalltalk

Jenkins

(90)

definitions values

modulus = 1000;

types

Count = nat inv c == c < modulus;

functions

succ : Count -> Count

succ(x) == (x + 1) mod modulus pre x < modulus

post RESULT < modulus;

state Counter of count : Count

inv mk_Counter(c) == c < modulus init s == s = mk_Counter(0) end

operations

get : () ==> Count get() == return count post RESULT < modulus;

inc : () ==> ()

inc() == count := succ(count);

reset : () ==> () reset() == count := 0;

end ExampleCounter

✡✝ ✆

4.8: Smalltalk VDM-SL

4.8 VDM-SL

1000 (modulus) (modular algebra)

succ modulus 1

count 0 3

get inc

1 resett 0

(91)

ViennaTranspiledObject subclass: #ExampleCounter slots: { #post_get. #inc. #Count. #Counter.

#init_Counter. #inv_Counter. #reset. #post_succ.

#state. #modulus. #get. #succ. #pre_succ.

#count => ViennaStateSlot } classVariables: { }

category: ’Auto Generated from VDM’

4.9: Smalltalk VDM-SL

ViennaTranspiledObject

VDM-SL

4.9

VDM-SL 4.3.4 ViennaType

4.8 Count

Count 4.10 Count VDM-SL

Smalltalk

ViennaTalk VDM-SL

Count nat inv c == c < modulo Smalltalk

ViennaType nat inv: [:c |

c < self modules] VDM-SL

Smalltalk

VDM-SL 4.3.3 4.2

4.8 modulus

(92)

ifNil: [ Count := ViennaTypeHolder new.

Count

type: (ViennaType nat

inv: [ :c | c < self modulus ]).

Count ]

4.10:

modulus ˆ modulus

ifNil: [ modulus := 1000.

modulus ]

4.11:

modulus 4.11

VDM-SL

Smalltalk

VDM-SL

ViennaTalk 4.12

succ succ pre succ post succ

succ 3 succ

(93)

succ ˆ succ

ifNil: [ pre_succ := [ :x | (self Count includes: x)

ifFalse: [ ViennaRuntimeTypeError signal ].

x < self modulus ].

post_succ := [ :x :RESULT | (self Count includes: x)

(self Count includes: RESULT)

RESULT < self modulus ].

succ := [ :x |

(self Count includes: x)

[ | RESULT |

RESULT := [ x < self modulus

ifFalse: [ ViennaPreconditionViolation signal ].

(x + 1) \\ self modulus ] value.

RESULT < self modulus

ifFalse: [ ViennaPostconditionViolation signal ].

RESULT ] value ].

succ ] 4.12:

succ ˆ succ

ifNil: [ pre_succ := [ :x | x < self modulus ].

post_succ :=

[ :x :RESULT | RESULT < self modulus ].

succ := [ :x | (x + 1) \\ self modulus ].

succ ] 4.13:

(94)

inv_Counter := [ :_inv |

| c |

(((ViennaRuntimeUtil matchTuple:

{(ViennaRuntimeUtil matchRecord: ’Counter’

args: {(ViennaRuntimeUtil matchIdentifier: ’c’)})}) value: {_inv})

ifEmpty: [ false ] ifNotEmpty: [ :binds |

c := binds first at: ’c’.

true ])

ifFalse: [ ViennaNoMatch signal ].

c < self modulus ]]

4.14:

ViennaTalk

succ 4.13

VDM-SL Smalltalk

4.9 VDM-SL count Smalltalk

count 4.8 Counter

ViennaTalk inv Counter

inv 4.14

inv Counter 4.15 inv

count inv

ViennaTalk

Pharo Smalltalk [VBLN11]

4.9

(95)

inv

(self inv_Counter value: self state)

ifFalse: [ self stateInvariantViolation ].

(self Count includes: count)

ifFalse: [ ViennaRuntimeTypeError signal ] 4.15:

ViennaStateSlot Smalltalk

count inv

Smalltalk ExampleCounter

count inv

count

VDM-SL Smalltalk

4.16 get

get: get

get

4.9 get

post get post get 4.17

4.4 VDMPad

ViennaTalk 1 VDMPad

VDMPad VDM-SL (IDE) [OA13, OAL15]

VDMPad IDE Web IDE

(96)

get: _op

| _oldState RESULT | _oldState := self state.

RESULT := self _get.

RESULT < self modulus

ifFalse: [ ViennaPostconditionViolation signal ].

ˆ RESULT _get

ˆ count get

ˆ get

ifNil: [ get := [ self get: nil ].

get ]

4.16:

post_get ˆ post_get

ifNil: [ post_get := [ :_State :_oldState :RESULT | (self Count includes: RESULT)

RESULT < self modulus ].

post_get ]

(97)

VDMPad VDM-SL

VDMPad

3.2 1

evaluate VDM

4.18 VDMPad

4.4.1

VDMPad VDM

VDM VDMPad

VDMJ Read-Eval-Print Loop

(REPL) REPL

Read

Eval Print

Loop

REPL VDM

VDM

(98)

仕様エリア

状態エリア

ワークスペース

結果エリア

メッセージエリア

(99)

VDM-SL

VDMPad

REPL VDMPad

VDM-SL VDM-SL

VDM-SL

VDM-SL 4.19

VDM-SL

evaluate VDM-SL

VDM-SL

VDMPad

evaluate

(100)

4.19:

VDMPad

VDM

VDMPad

4.4.2 VDM-SL

VDM-SL

4.18 VDMPad stock {<BEER> |-> 10, <WINE> |->

3}

(101)

real 1.0 quote <quote>

seq of char "abc"

seq [1, 2, 3, 4]

set {1, 2, 3, 4}

map {<one>|->1, <two>|->2 } product mk tuple(1, "abc")

composite mk Record(1, "abc")

token mk token(0)

4.20: VDMPad VDM-SL

3.2 2

4.20

4.4.3

VDMPad

VDMPad 3.2 3

(102)

単体テストの結果

4.21: VDMPad

4.4.4

3.3.6 xUnit

VDMPad

VDMPad VDMPad

VDMPad ON

evaluate make it a testcase 4.21

(103)

4.22:

4

4.22

make it a testcase

VDMPad

3.2 4

4.5 Lively Walk-Through

Lively Walk-Through UI

UI UI

UI

[NY13]

(104)

UI

Lively Walk-Through UI

UI UI

(105)

4.23: Lively Walk-Through

Lively Walk-Through 1

Lively Walk-Through

4.3.2 VDMBrowser

1 2

VDMBrowser

3

4 4.3.7

4.23 Lively Walk-Through VDM-

SL VDM-

Browser UI GUI

LiveTalk